proposition: Lemma sub_id : forall t, sub id t = t.
proof: Proof. set (P := fun t => sub id t = t). change (forall t, P t). apply term_ind_forall; intros; unfold P. refl. simpl. f_equal. apply Vmap_eq_id. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)