proposition: Lemma Cons_injective s s' u u': s ::: u = s' ::: u' -> s = s' /\ u = u'.
proof: Proof. injection 1; eauto. Qed.
imports: List Lia Program.Program Undecidability.HOU(std.std axioms) RelationClasses Morphisms Init.Wf Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.goldfarb.encoding) FinFun Coq.Arith.Wf_nat