proposition: Lemma af_to_af_lrel (X:Type) (A : X -> X -> Prop) : almost_full A -> almost_full_lrel (BinRelExtension A).
proof: Proof. intro afA. induction afA. apply AF_SUP. intros. apply AF_SUP. intro z. intros. apply AF_ZT. intros. right. right. simpl. apply H. apply AF_SUP. intro x. apply AF_SUP. intro y. apply (af_strengthen_lrel (H0 x)). intros. simpl in H1. destruct xs. destruct H1. destruct xs. simpl in H1. destruct H1. simpl in H1. destruct H1. left. left. auto. left. right. auto. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)