proposition: Lemma term_ind_forall : forall t, P t.
proof: Proof. apply term_ind_forall_cast. hyp. intro f. ded (is_unary_sig f). destruct ts. intro. lia. destruct ts. simpl Vforall. split_all. assert (h0 = is_unary_sig f). apply eq_unique. subst h0. apply Hfun. hyp. intro. lia. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)