Interaction of Backtrackings and Strict Constant Mappings on PreTrigger

We merely lift GroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs to PreTrigger here.

theorem PreTrigger.backtracking_under_constant_mapping_subset_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (trg : PreTrigger sig) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (trg_disjIdx_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (trg_rule_arity_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (trg_rule_in_rl : trg.rule ∈ rl.rules) : have backtracking := backtrackFacts rl trg trg_ruleIds_valid trg_disjIdx_valid trg_rule_arity_valid; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants rl.rules → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ backtracking.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ backtracking.snd then fresh_constant_remapping c else g c).apply_fact_set backtracking.fst.toSet ⊆ (backtrackFacts rl { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs } ⋯ ⋯ ⋯).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts rl { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs } ⋯ ⋯ ⋯).snd