proposition: Lemma foldeqs_typing Gamma E: Gamma ⊢₊₊(2) E : repeat (alpha → alpha → alpha) (length E) -> Gamma ⊢₂(2) (foldeqs E) : alpha → alpha → alpha.
proof: Proof. remember (repeat (alpha → alpha → alpha) (| E |)) as L. induction 1 in HeqL |- *; cbn. - repeat econstructor. - do 2 (destruct s; try solve [repeat econstructor]). do 2 (destruct t; try solve [repeat econstructor]). specialize (foldeqs_lambda_lambda E) as (u&v&H'); rewrite H' in *. cbn in HeqL. injection HeqL as -> ->. mp IHeqs_ordertyping; (eauto 2). inv H0. inv H4. inv H. inv H4. destruct IHeqs_ordertyping as [T1 T2]. inv T1. inv H4. inv T2. inv H4. repeat econstructor; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)