proposition: Lemma af_mut_induction_aux: 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: A+B, match a with | inl l => P l | inr r => Q r end.
proof: Proof. intros A B TA SA TB SB R Raf HTrans P Q fA fB. apply af_induction with (R := R) (T := @lift_rel_union _ _ TA TB SA SB). apply Raf. intros. eapply HTrans. apply H. intros. destruct x. apply fA. intros. remember (X (inl _ y)). simpl in y0. apply y0. apply H. intros. remember (X (inr _ y)). simpl in y0. apply y0. apply H. apply fB. intros. remember (X (inr _ y)). simpl in y0. apply y0. apply H. intros. remember (X (inl _ y)). simpl in y0. apply y0. apply H. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)