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 : alpha → alpha.
proof: Proof. intros. econstructor; trivial. inv H; inv H0. eapply AppL_ordertyping_repeated; auto. eapply orderlisttyping_preservation_under_renaming. eapply repeated_ordertyping; simplify. intros; mapinj. eapply encb_typing. all: eauto 2. intros ??; cbn; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)