Commit 6132d9f5 authored by François Thiré's avatar François Thiré

Fix comment

parent 89a5c94f
......@@ -266,7 +266,7 @@ Proof.
- split ; intro ; now apply IHConv.
- split ; intro.
+ inversion H0.
+ (* STUCK! Not provable... *) admit.
+ (* FALSE because t and u might not be typable *) admit.
- inversion H0 ; split ; intro ; subst.
+ exfalso ; eapply not_rel_kind_gamma_left ; eassumption.
+ exfalso ; eapply not_rel_kind_gamma_right ; eassumption.
......
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