generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
directed_relation_of_relation_class Left2Right ?
(apply_morphism ? ? m1 args1)
(apply_morphism ? ? m2 args2).
directed_relation_of_relation_class Left2Right ?
(apply_morphism ? ? m1 args1)
(apply_morphism ? ? m2 args2).
(directed_relation_of_argument_class
(get_rewrite_direction Left2Right t) t args1 args2);
generalize in match H1; clear H1;
(directed_relation_of_argument_class
(get_rewrite_direction Left2Right t) t args1 args2);
generalize in match H1; clear H1;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
generalize in match args1; clear args1;
generalize in match m2; clear m2;
generalize in match m1; clear m1;
Qed.
(* THE SAME EXAMPLES ON impl *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
Qed.
(* THE SAME EXAMPLES ON impl *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.