fact: Parameter subst_trivial_ext : forall vars sigma t, apply_subst (extend_with_id vars sigma) t = apply_subst sigma t.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)