proposition: Lemma prv_transport_to_falsity A phi : A ⊢ phi -> (map to_falsity A) ⊢ (to_falsity phi).
proof: Proof. intros H; induction H. - cbn. apply II. apply IHprv. - cbn. eapply IE. 1: now apply IHprv1. now apply IHprv2. - cbn. apply AllI. rewrite map_map in *. erewrite map_ext. 1: now apply IHprv. intros a. rewrite <- ! subst_falsity_id. rewrite subst_falsity_comm. now cbn. - rewrite <- subst_falsity_id. change (⊥) with (⊥[t..]). rewrite <- subst_falsity_comm. apply AllE. rewrite subst_falsity_id. now apply IHprv. - apply Exp. apply IHprv. - apply Ctx. now apply in_map. - apply Pc. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts