proposition: Lemma clos_trans_of_clos_trans1 A (r r' : relation A) x y : (fun a b => r⁺ a b \/ r' a b)⁺ x y <-> (fun a b => r a b \/ r' a b)⁺ x y.
proof: Proof. split; induction 1; desf; eauto using clos_trans, clos_trans_mon. Qed.
imports: HahnBase HahnList Relations