proposition: Theorem af_induction: forall (A:Type) (T : A -> A -> Prop) (R : A -> A -> Prop), almost_full R -> (forall x y, clos_trans_1n A T x y /\ R y x -> False) -> forall P : A -> Type, (forall x, (forall y, T y x -> P y) -> P x) -> forall a, P a.
proof: Proof. intros A T R AF Disj P g. apply well_founded_induction_type with (R := T). destruct AF as (p,HSec); apply wf_from_af with (R := R) (p := p). apply Disj. apply HSec. apply g. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.Default(AlmostFull) AlmostFull.Default(AFConstructions)