proposition: Lemma HGamma₀s₀A₀ (S: list card) : [Arr (repeat (alpha → alpha) (length S)) alpha; (alpha → alpha) → alpha] ⊢( 3) (lambda lambda lambda h (AppR f (Enc 1 2 (heads S))) (AppR f (repeat (var (u 1)) (length S)))) : ((alpha → alpha) → (alpha → alpha) → (alpha → alpha → alpha) → alpha).
proof: Proof. do 4 econstructor. econstructor. econstructor; cbn; trivial; cbn; trivial. - eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S) ); simplify. erewrite <-map_length; eapply Enc_typing. all: econstructor; trivial. simplify; cbn; eauto. - eapply AppR_ordertyping. + eapply repeated_ordertyping; simplify; [|eauto]. intros s H'. eapply repeated_in in H'. subst. econstructor; cbn. 2: eauto. eauto. + econstructor; simplify; auto. 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)