proposition: Lemma af_strengthen_lrel (X:Type) (A : LRel X) : almost_full_lrel A -> forall (B : LRel X), (forall xs, A xs -> B xs) -> almost_full_lrel B.
proof: Proof. intro afA. induction afA. intros. apply AF_ZT. intros. apply H0. apply H. intros. apply AF_SUP. intros. apply H0 with (x := x). intros. destruct H2. left. apply H1. apply H2. right. apply H1. apply H2. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)