proposition: Lemma beq_terms : forall n (ts : terms n) p (us : terms p), (fix beq_terms n (ts : terms n) p (us : terms p) := match ts, us with | Vnil, Vnil => true | Vcons t ts', Vcons u us' => beq_term t u && beq_terms _ ts' _ us' | _, _ => false end) _ ts _ us = beq_vec beq_term ts us.
proof: Proof. induction ts; destruct us; refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)