Commit e7d3a2cf authored by Ulrich's avatar Ulrich

fixed the coq8.6 issue

parent 0e730222
......@@ -404,11 +404,15 @@ Proof with trivial.
apply sub_closed_empty...
+ apply (eq_split_right (ggr_dneg_eq _ _ _)).
- eauto 4 with KIboxDB.
- intuition.
eapply eq_ded in H; try eapply or_dneg.
eq_rewrite2 ggr_dneg_eq.
push_left. apply_imp_ass.
+ eq_rewrite1 and_or_neg.
- assert (KIbox Z [] (ggr Z)) as HgZ2; trivial.
assert (KIbox Z [] (ggr Z)) as HgZ3; trivial.
apply IHHGA1 in HgZ; trivial.
apply IHHGA2 in HgZ2; trivial.
apply IHHGA3 in HgZ3; trivial.
eapply eq_ded in HgZ; try eapply or_dneg.
eq_rewrite2 ggr_dneg_eq.
push_left. apply_imp_ass.
+ eq_rewrite1 and_or_neg.
eapply box_andI; push_left; elim_false (ggr f3).
* permute_context perm_takeit_6. stronger_assumption.
* permute_context perm_takeit_6. stronger_assumption.
......
......@@ -52,6 +52,12 @@
\maketitle
\end{frame}
%\begin{frame}
% \title[Chicken]{Chicken chicken chicken}
% \
% \maketitle
%\end{frame}
%\begin{frame}
% Miri: \\
% Einführung, was ist KIbox?
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment