proposition: Lemma sty_ind' (P : sty -> Prop) : (forall x, P (atom x)) -> (forall s phi t, P s -> Forall P phi -> P t -> P (arr s phi t)) -> forall s, P s.
proof: Proof. move=> IH1 IH2. elim /(Nat.measure_induction _ sty_size). case. - move=> *. apply: IH1. - move=> s phi t IH'. apply: IH2. + apply: IH'=> /=. lia. + elim: phi IH'; first done. move=> s' phi' IH1' IH2'. constructor. * apply: IH2'=> /=. lia. * apply: IH1'=> /= *. apply: IH2'=> /=. lia. + apply: IH'=> /=. lia. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect