proposition: Lemma forward_typing theta: nil ⊩( 3) encs theta : Gamma__dwk E.
proof: Proof. intros ?? <- % nth_error_In % repeated_in. eapply typing_enc. Qed.
imports: List Arith Lia Undecidability.HOU(std.std calculus.calculus) Undecidability.HOU.second_order(diophantine_equations dowek.encoding) Undecidability.HOU.unification.nth_order_unification