Skip to content

feat(Tactic/Simproc): support Prop-valued dependent quantifiers in existsAndEq - #43059

Open
vasnesterov wants to merge 7 commits into
leanprover-community:masterfrom
vasnesterov:existsAndEq_dependent
Open

feat(Tactic/Simproc): support Prop-valued dependent quantifiers in existsAndEq#43059
vasnesterov wants to merge 7 commits into
leanprover-community:masterfrom
vasnesterov:existsAndEq_dependent