proposition: Lemma ext_allfv_subst_term sigma1 sigma2 t : allfv (fun x=> sigma1 x = sigma2 x) t -> subst sigma1 t = subst sigma2 t.
proof: Proof. elim: t sigma1 sigma2. - by move=> > /= ?. - by move=> ? IH1 ? IH2 ?? /= [/IH1 -> /IH2 ->]. - move=> ? IH > /= Hsigma. congr lam. apply: IH. apply: allfv_impl Hsigma. by move=> [|x] /= => [|->]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect