proposition: Lemma subterm_eq_proj : forall t, subterm_eq (proj t) t.
proof: Proof. intro. case t. simpl. intro. refl. simpl. intros. case (zerop (arity f)). intros. refl. intros. apply subterm_strict. apply subterm_fun. apply Vnth_in. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)