proposition: Lemma Var_subst : forall n e t F, t ⊩ F -> get n e = t -> n↓e ⊩ F.
proof: Proof. intros n e t F Ht Hget π Hπ. eapply anti_evaluation. apply red_Var. rewrite Hget. now apply Ht. Qed.
imports: ClassicalRealizability.ShallowEmbedding