proposition: Corollary af_intersection_usual (X:Type) (A : X -> X -> Prop) (B : X -> X -> Prop) : almost_full A -> almost_full B -> almost_full (fun x y => A x y /\ B x y).
proof: Proof. intros. assert (almost_full_lrel (BinRelExtension A)). apply af_to_af_lrel. apply H. assert (almost_full_lrel (BinRelExtension B)). apply af_to_af_lrel. apply H0. assert (almost_full_lrel (fun ys => BinRelExtension A ys /\ BinRelExtension B ys)). eapply af_intersection_lrel_cor with (p := SUP (fun _ => SUP (fun _ => @ZT X))). simpl. firstorder. simpl. firstorder. apply H1. apply H2. assert (almost_full_lrel (fun ys => BinRelExtension (fun x y => A x y /\ B x y) ys)). apply (af_strengthen_lrel H3). intros. destruct H4. destruct xs. simpl. destruct H4. destruct xs. destruct H4. simpl. simpl in H5. simpl in H5. auto. apply af_lrel_to_af_cor. apply H4. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)