proposition: Lemma sat_ext_bounded_term t rho sigma : (forall x, ~ bounded_indi_term x t -> get_indi rho x = get_indi sigma x) -> (forall x ar, ~ bounded_func_term ar x t -> get_func rho x ar = get_func sigma x ar) -> eval rho t = eval sigma t.
proof: Proof. intros H1 H2. induction t; cbn. - apply H1. cbn. lia. - rewrite H2. f_equal. apply map_ext_in. intros t H. eapply Forall_in in IH. apply IH. intros x H3. apply H1. cbn. intros H4. apply H3. eapply Forall_in in H4. apply H4. trivial. intros x ar' H3. apply H2. cbn. intros [H4 H5]. apply H3. eapply Forall_in in H5. apply H5. easy. easy. cbn. lia. - f_equal. apply map_ext_in. intros t H. eapply Forall_in in IH. apply IH. intros x H3. apply H1. cbn. intros H4. apply H3. eapply Forall_in in H4. apply H4. trivial. intros x ar' H3. apply H2. cbn. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy. easy. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector