proposition: Lemma trans_with_eq : forall A (R : relation A) a1 a2, trans_clos (union A (@eq _) R) a1 a2 <-> refl_trans_clos R a1 a2.
proof: Proof. intros A R a1 a2; split. intro H; induction H as [b1 b2 H | b1 b2 b3 H1 H2]. destruct H as [H | H]. subst b2; apply r_step; assumption. apply t_clos; apply t_step; assumption. destruct H1 as [H1 | H1]. subst b2; assumption. destruct IHH2 as [b2 | b2 b3 H3]. apply t_clos; apply t_step; assumption. apply t_clos; apply t_trans with b2; assumption. intro H; destruct H as [a1 | a1 a2 H]. apply t_step; left; apply eq_refl. apply (@trans_incl _ R); trivial. right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)