proposition: Lemma union_rel_rt1_left A (R S : rel A) : R#1 << (R U S)#1.
proof: Proof. intros x y xRy. induction xRy. refl. apply rt1_trans with y. left. hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)