proposition: Lemma af_lrel_to_af (X:Type) (R : LRel X) : (forall x y zs, R (x :: y :: zs) <-> R (x :: y :: nil)) -> almost_full_lrel R -> almost_full (fun x y => R (x :: y :: nil)).
proof: Proof. intros. induction H0. intros. apply AlmostFull.AF_ZT. intros. apply H0. apply AlmostFull.AF_SUP. intro x. assert ((forall (x0 y : X) (zs : list X), R (x0 :: y :: zs) \/ R (x :: x0 :: y :: zs) <-> R (x0 :: y :: nil) \/ R (x :: x0 :: y :: nil))). intros. split. intros. destruct H2. left. remember (H x0 y zs). destruct i. apply r. apply H2. right. assert (R (x::x0::nil)). remember (H x x0 (y::zs)). destruct i. apply r. apply H2. remember (H x x0 (y::nil)). destruct i. apply r0. apply H3. intros. destruct H2. left. destruct (H x0 y zs). apply H4. apply H2. right. destruct (H x x0 (y::zs)). apply H4. destruct (H x x0 (y::nil)). apply H5. apply H2. apply (af_strengthen (H1 x H2)). intros. destruct H3. left. auto. right. destruct (H x x0 (y::nil)). apply H4. apply H3. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)