proposition: Lemma trans_incl : forall A (R1 R2 : relation A), inclusion _ R1 R2 -> inclusion _ (trans_clos R1) (trans_clos R2).
proof: Proof. intros A 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 b'; trivial. apply R1_in_R2; trivial. Qed.
imports: Coq(Setoid Relations List Utf8)