proposition: Lemma allfv_dec P M : (forall x, P x \/ not (P x)) -> allfv P M \/ not (allfv P M).
proof: Proof. elim: M P=> /=. - done. - move=> s IH1 t IH2 ? /[dup] /IH1 {}IH1 /IH2 {}IH2. tauto. - move=> ? IH P H. case: (IH (scons True P)); [|by auto..]. move=> [|?] /=; by auto. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect