Supporting results for pointwise provable equality.

Composition on program quotients and its obstruction.

theorem PointwiseComposition.FailureOfComposition.quotient_composition_exists_iff {A : Type u} (s : Setoid A) (comp : A → A → A) : (∃ (C : Quotient s → Quotient s → Quotient s), ∀ (a b : A), C (Quotient.mk s a) (Quotient.mk s b) = Quotient.mk s (comp a b)) ↔ ∀ (a a' b b' : A), Setoid.r a a' → Setoid.r b b' → Setoid.r (comp a b) (comp a' b')

A binary operation descends to a quotient exactly when it preserves the equivalence relation in both arguments.