proposition: Lemma dn_forall {F} Gamma phi : F[↑] = F -> Gamma ⊢M dn F (∀ phi) → ∀ dn F phi.
proof: Proof. intros HF. apply II. constructor. apply II. cbn. change ((∀ phi[up ↑])) with ((∀ phi)[↑]). rewrite !HF. eapply IE with (phi:= _ → _). { apply Ctx; auto. right. left. easy. } apply II. eapply IE with (phi:= phi). { apply Ctx; auto. right. left. easy. } cbn. rewrite <-form_up_var0_invar. apply AllE, Ctx; auto. left. easy. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FullSyntax) Undecidability.FOL.Arithmetics(Robinson NatModel)