proposition: Lemma fin_union_spec {A n} (f : fin n -> relation A) : forall x y, fin_union f x y <-> exists k, f k x y.
proof: Proof. intros x y. funelim (fin_union f). split. intros []. intros [k _]. depelim k. split. intros [Hfz|Hfs]. now exists fz. specialize (H x y x y). rewrite -> H in Hfs. destruct Hfs. now exists (fs x0). intros [k Hk]. depelim k. intuition. right. rewrite (H x y). now exists k. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect