definition false_f \def \lambda (X:Type). \lambda (_:X). False.
record Class: Type \def {
- class: Type;
+ class:> Type;
cin : class \to Prop;
cle1 : class \to class \to Prop
}.
-coercion class.
-
inductive ceq (C:Class) (c1:C): C \to Prop \def
| ceq_refl: cin ? c1 \to ceq ? c1 c1
| ceq_sing_r: \forall c2,c3.