proposition: Lemma seqA2 A (r r' r'' : relation A) x y : ((r⨾ r')⨾ r'') x y <-> (r⨾ r'⨾ r'') x y.
proof: Proof. unfold seq; split; ins; desf; eauto 8. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets