proposition: Lemma type_eqb_true: forall t1 t2, type_eqb t1 t2 = true -> t1 = t2.
proof: Proof. induction t1; intros; destruct t2; simpl in *; try congruence. apply Bool.andb_true_iff in H. destruct H. f_equal; eauto. Qed.
imports: Arith Lia List