proposition: Lemma lin_typing Gamma S t: (Gamma ⊢₊(2) S : repeat alpha (length S)) -> (Gamma ⊢(2) t : alpha) -> Gamma ⊢(2) lin S t : alpha.
proof: Proof. intros ? ?. induction S as [|s S IH]; simplify; [auto|]. inv H. econstructor; cbn; eauto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)