-nlemma cconv_cdiv_false: ∀c,d,e. cconv c e → cdiv c d → False.
- #c d e K; nelim K
- [##1,2: #U; ninversion U; #; ndestruct
- |##*: /3/]
-nqed.
-
-ndefinition ceq ≝ λc1,c2. cconv c1 c2 ∨ cdiv c1 c2.
-
-ndefinition committed ≝ λc. ceq c c.
-
-nrecord cval : Type[0] ≝ {
- ccarr:> cprop;
- ccomm: committed ccarr
-}.
-
-ntheorem ceq_refl: ∀c:cval. ceq c c.
- //.
-nqed.
-
-nlet corec cdiv_sym c d (K: cdiv c d) : cdiv d c ≝ ?.
- ncases K; /3/.
-nqed.
-
-nlet rec cconv_sym c d (K: cconv c d) on K : cconv d c ≝ ?.
- ncases K; /3/.
-nqed.
-
-ntheorem ceq_sym: ∀c,d:cval. ceq c d → ceq d c.
- #x; ncases x; #c Kc; #y; ncases y; #d Kd;
- ncases Kc; #K1; *; /3/.
+nlemma ceq_to_cconv2: ∀c,b. ceq (certain b) c → cconv (certain b) c.
+ #c b K; ninversion K; #; ndestruct; //.