proposition: Lemma trans_incl2 : forall A B (f : A -> B) (R1 : relation A) (R2 : relation B), (forall a1 a2, R1 a1 a2 -> R2 (f a1) (f a2)) -> forall a1 a2, trans_clos R1 a1 a2 -> trans_clos R2 (f a1) (f a2).
proof: Proof. intros A B f R1 R2 R1_in_R2 a b H; induction H as [a' b' H | a' b' c' H1 H2]. apply t_step; apply R1_in_R2; trivial. apply t_trans with (f b'); trivial. apply R1_in_R2; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)