Jan van Brügge (Jul 26 2022 at 13:31): Jan van Brügge (Jul 26 2022 at 13:31):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) ∪ {}) = {}
What am I doing wrong?
Last updated: Sep 28 2026 at 16:33 UTC