Failing to solve existential goal but metis can · Beginner Questions

Hi, I am trying to solve a goal involving existentials. The proofs is provable by metis, but for what I want to do I need to do it without any fancy proof methods, only unfolding/rule/erule/etc. I simply fail to solve it. The goal in question is this:

using this:
  ∃u. bij u ∧ |supp u| <o |UNIV| ∧ imsupp u ∩ (FFVars_τ (τ_ctor ?x) ∪ imsupp (Rep_ssfun ?p) ∪ {} - set2_τ_pre ?x) = {} ∧ u ` set2_τ_pre ?x ∩ (FFVars_τ (τ_ctor ?x) ∪ imsupp (Rep_ssfun ?p) ∪ {}) = {}

goal (1 subgoal):
 1. ∃pick.
       ∀x p. bij (pick x p) ∧
             |supp (pick x p)| <o |UNIV| ∧
             imsupp (pick x p) ∩ (FFVars_τ (τ_ctor x) ∪ imsupp (Rep_ssfun p) ∪ {} - set2_τ_pre x) = {} ∧ pick x p ` set2_τ_pre x ∩ (FFVars_τ (τ_ctor x) ∪ imsupp (Rep_ssfun p) ∪ {}) = {}

Stream: Beginner Questions

Topic: Failing to solve existential goal but metis can

Jan van Brügge (Jul 26 2022 at 13:31):