proposition: Lemma eterm_ind' (P : eterm -> Prop) : (forall (l : list eterm) (t : term), Forall P l -> P (closure l t)) -> forall u, P u.
proof: Proof. move=> H. elim /(Nat.measure_induction _ eterm_size). move=> [ctx t] IH. apply: H. elim: ctx IH. - by constructor. - move=> ?? IH IH'. constructor. + apply: IH'=> /=. lia. + apply: IH => /= *. apply: IH'=> /=. lia. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect