proposition: Lemma af_intersection_lrel (X:Type): forall (p : WFT X), forall (R : LRel X), almost_full_lrel R -> forall (T : LRel X), almost_full_lrel T -> forall (C : LRel X), forall A B, Arity p A -> Arity p B -> (forall xs, R xs -> C xs \/ A xs) -> (forall xs, T xs -> C xs \/ B xs) -> almost_full_lrel (fun xs => C xs \/ A xs /\ B xs).
proof: Proof. intro p. induction p. intros R afR. induction afR. intros. apply (af_strengthen_lrel H0). intros. destruct (H4 xs H5). left; auto. destruct (H3 xs (H xs)). left; auto. right; auto. intros. apply AF_SUP. intros. remember (H0 x T H1 (fun ys => C ys \/ C (x::ys))) as G. clear HeqG. clear H0. assert(almost_full_lrel (X:=X) (fun xs : list X => (fun ys : list X => C ys \/ C (x :: ys)) xs \/ A xs /\ B xs)). apply G. apply H2. apply H3. intros. destruct H0. destruct (H4 xs H0). left. left. auto. right. auto. destruct (H4 (x::xs) H0). left. right; auto. simpl in H2. destruct (H2 (x::xs)). assert (A nil). apply H7. apply H6. right. destruct (H2 xs). apply H11. apply H9. intros. destruct (H5 xs H0). left. left. auto. right. auto. apply (af_strengthen_lrel H0). intros. destruct H6. destruct H6. left. left. auto. right. left. auto. left. right. auto. intros R afR. induction afR. intros. apply (af_strengthen_lrel H1). intros. destruct (H5 xs H6). left. auto. destruct (H4 xs (H0 xs)). left. auto. right; auto. intros T afT. induction afT. assert (almost_full_lrel R). apply (AF_SUP H0). intros. apply (af_strengthen_lrel H3). intros. destruct (H6 xs H8). left; auto. destruct (H7 xs (H2 xs)). left. auto. right; auto. intros. apply AF_SUP. intro x. assert (almost_full_lrel R) as afR. apply (AF_SUP H0). assert (almost_full_lrel R0) as afR0. apply (AF_SUP H2). assert (almost_full_lrel (fun ys => ((C ys \/ C (x::ys) \/ (A ys /\ B ys)) \/ A (x::ys)))) as GLeft. eapply af_strengthen_lrel. apply (H1 x R0 afR0 (fun ys => C ys \/ C (x::ys) \/ A (x::ys)) A B H4 H5). intros. destruct H8. destruct (H6 xs H8). left. left. auto. right. auto. destruct (H6 (x::xs) H8). left. right. left. auto. left. right. auto. intros. destruct (H7 xs H8). left. left. auto. right. auto. intros. destruct H8. destruct H8. left. auto. destruct H8. left. right. left. auto. right. auto. left. right. auto. assert (almost_full_lrel (fun ys => ((C ys \/ C (x::ys) \/ (A ys /\ B ys)) \/ B (x::ys)))) as GRight. eapply af_strengthen_lrel. apply (H3 x (fun ys => C ys \/ C (x::ys) \/ B (x::ys)) A B H4 H5). intros. destruct (H6 xs H8). left. left. auto. right. auto. intros. destruct H8. destruct (H7 xs H8). left. left. auto. right. auto. destruct (H7 (x::xs) H8). left. right. left. auto. left. right. auto. intros. destruct H8. destruct H8. left. auto. destruct H8. left. right. left. auto. right. auto. left. right. right. auto. eapply af_strengthen_lrel. eapply (@H x (fun ys => (C ys \/ C (x::ys) \/ (A ys /\ B ys)) \/ A (x::ys)) GLeft (fun ys => (C ys \/ C (x::ys) \/ (A ys /\ B ys)) \/ B (x::ys)) GRight (fun ys => C ys \/ C (x::ys) \/ A ys /\ B ys) (fun ys => A (x::ys)) (fun ys => B (x::ys))). apply H4. apply H5. 3: { intros. destruct H8. destruct H8. left. left. auto. destruct H8. right. left. auto. left. right; auto. right. auto. } auto. auto. Defined.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)