proposition: Lemma Enc_typing (Gamma: ctx) W: (Gamma ⊢(3) @var X u : alpha → alpha) -> (Gamma ⊢(3) @var X v : alpha → alpha) -> Gamma ⊢₊(3) Enc W : repeat (alpha → alpha) (length W).
proof: Proof. intros. eapply repeated_ordertyping; simplify; trivial. intros; mapinj. eapply enc_typing; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)