- intros 2;
- elim R 0;
- simplify;
- [1,2: intros 4; apply r
- |3,4: intros 3; apply r
- | intros 1 (T1); apply (eq T1).
- (* this eta expansion is needed to avoid a universe inconsistency *)
- ]
-qed.
-
-definition relation_of_relation_classCOQ:
- ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2;
- exact (
- match
- R
- return
- (λ x.carrier_of_relation_class X x -> carrier_of_relation_class X x -> Prop)
-with [
- SymmetricReflexive A Aeq _ _ => Aeq
-| AsymmetricReflexive _ A Aeq _ => Aeq
-| SymmetricAreflexive A Aeq _ => Aeq
-| AsymmetricAreflexive _ A Aeq => Aeq
-| Leibniz T => eq T]).
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]