proposition: Lemma subst_trivial_ext : forall vars sigma t, apply_subst (extend_with_id vars sigma) t = apply_subst sigma t.
proof: Proof. unfold extend_with_id. intros vars sigma t; rewrite <- subst_eq_vars. intros v _; simpl; rewrite find_app. case_eq (mem_bool X.eq_bool v (map (fun st : variable * term => fst st) (map (fun x : variable => (x, Var x)) (filter (fun x : variable => negb (mem_bool X.eq_bool x (map (@fst _ _) sigma))) vars)))); [intro v_in | intros _; apply eq_refl]. case_eq (find X.eq_bool v (map (fun x : variable => (x, Var x)) (filter (fun x : variable => negb (mem_bool X.eq_bool x (map (@fst _ _) sigma))) vars))); [intros x' F | intro F]. destruct (find_mem _ _ X.eq_bool_ok _ _ F) as [v' [l1 [l2 [v_eq_v' H]]]]; subst v'. assert (v_in' : In (v,x') (l1 ++ (v,x') :: l2)). apply in_or_app; right; left; apply eq_refl. rewrite <- H in v_in'. rewrite in_map_iff in v_in'. destruct v_in' as [v' [v_eq_v' v_in']]; injection v_eq_v'; clear v_eq_v'; do 2 intros; subst v' x'. rewrite filter_In in v_in'. destruct v_in' as [_ v_in']. case_eq (find X.eq_bool v sigma); [intros v_val v_sigma | intros _; apply eq_refl]. apply False_rect. destruct (find_mem _ _ X.eq_bool_ok _ _ v_sigma) as [v' [sig1 [sig2 [v_eq_v' H']]]]; subst v'. rewrite H' in v_in'; clear - v_in'; induction sig1 as [ | [u u'] sig1]; simpl in v_in'. rewrite eq_var_bool_refl in v_in'; discriminate. destruct (eq_var_bool v u); [discriminate | apply IHsig1 ; assumption]. assert (v_mem := mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : variable * term => fst st) (map (fun x : variable => (x, Var x)) (filter (fun x : variable => negb (mem_bool eq_var_bool x (map (@fst _ _) sigma))) vars)))); rewrite v_in in v_mem. assert (v_in'' := mem_impl_in (@eq variable) (fun a b P => P) _ _ v_mem). rewrite in_map_iff in v_in''; destruct v_in'' as [[v' u] [v_eq_v' v_in3]]; simpl in v_eq_v'; subst v'. apply False_rect; refine (find_not_found X.eq_bool v v _ _ F (eq_var_bool_refl v) v_in3). Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)