proposition: Lemma af_intersection_lrel_cor (X:Type): forall (p : WFT X) A B, Arity p A -> Arity p B -> almost_full_lrel A -> almost_full_lrel B -> almost_full_lrel (fun xs => A xs /\ B xs).
proof: Proof. intros. pose (C := fun (ys : list X) => False). assert (almost_full_lrel (fun xs => C xs \/ (A xs /\ B xs))). apply af_intersection_lrel with (p := p) (R := A) (T := B). apply H1. apply H2. apply H. apply H0. auto. auto. apply (af_strengthen_lrel H3). intros. auto. destruct H4. destruct H4. auto. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)