proposition: Corollary af_interesection {X : Type} (A B : X -> X -> Prop) : AlmostFull A -> AlmostFull B -> AlmostFull (inter_rel A B).
proof: Proof. intros [pa Ha] [pb Hb]. exists (oplus_binary pa pb). now apply oplus_binary_sec_intersection. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)