proposition: Lemma encb_typing (Gamma: ctx) b: (Gamma ⊢(3) @var X u : alpha → alpha) -> (Gamma ⊢(3) @var X v : alpha → alpha) -> Gamma ⊢(3) encb b : (alpha → alpha).
proof: Proof. intros H1 H2. destruct b; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)