proposition: Lemma af_mut_induction: forall (A:Type) (B:Type) (TA : A -> A -> Prop) (SA : A -> B -> Prop) (TB : B -> B -> Prop) (SB : B -> A -> Prop) (R : A + B -> A + B -> Prop), almost_full R -> (forall x y, @clos_trans_1n (A+B) (@lift_rel_union _ _ TA TB SA SB) x y /\ R y x -> False) -> forall (P : A -> Type) (Q : B -> Type), (forall x : A, (forall y, TA y x -> P y) -> (forall y, SB y x -> Q y) -> P x) -> (forall x : B, (forall y, TB y x -> Q y) -> (forall y, SA y x -> P y) -> Q x) -> (forall a, P a) * (forall b, Q b).
proof: Proof. intros. assert (forall a:A+B, match a with | inl l => P l | inr r => Q r end). eapply af_mut_induction_aux. apply H. apply H0. apply X. apply X0. split. intros. remember (X1 (inl _ a)). auto. intros. remember (X1 (inr _ b)). auto. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)