proposition: Lemma HGamma₀t₀A₀ (S: list card) : [Arr (repeat (alpha → alpha) (length S)) alpha; (alpha → alpha) → alpha] ⊢( 3) (lambda lambda lambda h (AppR f (Enc 1 2 (tails S))) (var (u 1) (g (var (u 1))))) : ((alpha → alpha) → (alpha → alpha) → (alpha → alpha → alpha) → alpha).
proof: Proof. Proof with cbn [ord' ord alpha]; simplify; cbn; (auto 2). do 4 econstructor. econstructor. econstructor; (auto 2)... cbn. lia. 2: do 2 econstructor... 2 - 3: econstructor... eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S)); simplify. erewrite <-map_length; eapply Enc_typing. all: econstructor; trivial; simplify; cbn; lia. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)