-(* COMMENTS
-Initial nodes: 199
-END *)
-
-theorem clear_mono:
- \forall (c: C).(\forall (c1: C).((clear c c1) \to (\forall (c2: C).((clear c
-c2) \to (eq C c1 c2)))))
-\def
- \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (c1: C).((clear c0 c1) \to
-(\forall (c2: C).((clear c0 c2) \to (eq C c1 c2)))))) (\lambda (n:
-nat).(\lambda (c1: C).(\lambda (_: (clear (CSort n) c1)).(\lambda (c2:
-C).(\lambda (H0: (clear (CSort n) c2)).(clear_gen_sort c2 n H0 (eq C c1
-c2))))))) (\lambda (c0: C).(\lambda (H: ((\forall (c1: C).((clear c0 c1) \to
-(\forall (c2: C).((clear c0 c2) \to (eq C c1 c2))))))).(\lambda (k:
-K).(\lambda (t: T).(\lambda (c1: C).(\lambda (H0: (clear (CHead c0 k t)
-c1)).(\lambda (c2: C).(\lambda (H1: (clear (CHead c0 k t) c2)).(K_ind
-(\lambda (k0: K).((clear (CHead c0 k0 t) c1) \to ((clear (CHead c0 k0 t) c2)
-\to (eq C c1 c2)))) (\lambda (b: B).(\lambda (H2: (clear (CHead c0 (Bind b)
-t) c1)).(\lambda (H3: (clear (CHead c0 (Bind b) t) c2)).(eq_ind_r C (CHead c0
-(Bind b) t) (\lambda (c3: C).(eq C c1 c3)) (eq_ind_r C (CHead c0 (Bind b) t)
-(\lambda (c3: C).(eq C c3 (CHead c0 (Bind b) t))) (refl_equal C (CHead c0
-(Bind b) t)) c1 (clear_gen_bind b c0 c1 t H2)) c2 (clear_gen_bind b c0 c2 t
-H3))))) (\lambda (f: F).(\lambda (H2: (clear (CHead c0 (Flat f) t)
-c1)).(\lambda (H3: (clear (CHead c0 (Flat f) t) c2)).(H c1 (clear_gen_flat f
-c0 c1 t H2) c2 (clear_gen_flat f c0 c2 t H3))))) k H0 H1))))))))) c).
-(* COMMENTS
-Initial nodes: 357
-END *)