Distributes universal quantifiers over a conjunction at the end of a binder telescope.
If e is ∀ x₁ … xₙ, a ∧ b, where at least one binder is dependent (a genuine ∀, not an
arrow), returns (lhs, rhs, h) with lhs := ∀ x₁ … xₙ, a, rhs := ∀ x₁ … xₙ, b, and
h : e = (lhs ∧ rhs).
∀ x, p x ∧ q x is split so that each conjunct gets its own E-matching pattern, and the arrows
in ∀ x, p x → q x ∧ r x must not block that. A telescope of arrows alone, p → a ∧ b, is
kept: grind propagates a ∧ b from p without a case split.
Equations
- One or more equations did not get rendered due to their size.