fact: Parameter well_formed_remove_term : forall sigma t, well_formed (apply_subst sigma t) -> forall x, var_in_term x t = true -> well_formed (apply_subst sigma (Var x)).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)