proposition: Lemma normalise_subst Delta sigma: Delta ⊩ sigma : Gamma -> { tau | (forall x, sigma x >* tau x) /\ (forall x, x ∈ dom Gamma -> normal (tau x)) /\ Delta ⊩ tau : Gamma}.
proof: Proof. intros T. assert (forall x, x ∈ dom Gamma -> { A | nth Gamma x = Some A }) as I. { intros x H1. destruct nth eqn: ?; eauto. exfalso. domin H1. congruence. } exists (fun x => match x el dom Gamma with | left H => eta (sigma x) (T _ _ (proj2_sig (I x H))) | right _ => sigma x end). split; [| split]. 1-2: intros x; destruct dec_in; intuition trivial. eapply eta_correct. eapply eta_normal. intros x B H. destruct dec_in; [|eauto]. destruct I; cbn. generalize (T x x0 e). rewrite H in e; injection e as ->. eapply eta_typing. Qed.
imports: List Lia Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order evaluator)