- ∀dir (R: Argument_Class).
- carrier_of_relation_class R → carrier_of_relation_class R → Prop.
- intros dir R.
- rewrite <-
- (about_carrier_of_relation_class_and_relation_class_of_argument_class R).
- exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)).
+ ∀dir:rewrite_direction.∀R: Argument_Class.
+ carrier_of_relation_class ? R → carrier_of_relation_class ? R → Prop.
+ intros (dir R);
+ generalize in match
+ (about_carrier_of_relation_class_and_relation_class_of_argument_class R);
+ intro H;
+ apply (directed_relation_of_relation_class dir (relation_class_of_argument_class R));
+ apply (eq_rect ? ? (λX.X) ? ? (sym_eq ? ? ? H));
+ [ apply c
+ | apply c1
+ ]