proposition: Lemma list_union_app {A} (rs rs' : list (relation A)) : forall x y, list_union (rs ++ rs') x y <-> list_union rs x y \/ list_union rs' x y.
proof: Proof. induction rs; intros; simpl; simp list_union; intuition. rewrite -> IHrs in H0. intuition. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect