proposition: Lemma refl_trans_incl : forall A (R1 R2 : relation A), inclusion _ R1 R2 -> inclusion _ (refl_trans_clos R1) (refl_trans_clos R2).
proof: Proof. intros A R1 R2 R1_in_R2 a b [a' | a' b' H]. left. apply t_clos; apply trans_incl with R1; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)