proposition: Corollary af_lrel_to_af_cor (X:Type) (A : X -> X -> Prop) : almost_full_lrel (BinRelExtension A) -> almost_full A.
proof: Proof. intros. apply af_strengthen with (A := fun x y => BinRelExtension A (x::y::nil)). apply af_lrel_to_af. intros. simpl. auto. split. intros. auto. intros. auto. apply H. intros. simpl in H0. auto. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)