lean2/tests/lean/defeq_simplifier1.lean.expected.out

λ (x y z w : A), q (q (q w))
A → A → A → (∀ (w : A), q (q (q w)) = w)
λ (x y z w : A), q (f (q (q x)) (q (q z)) (q w))
∀ (x : A), A → (∀ (z w : A), q (f (q (q x)) (q (q z)) (q w)) = w)
λ (x y z w : A), q (q (q w))
A → A → A → (∀ (w : A), q (q (q w)) = w)
λ (x y z w : A), w
A → A → A → (∀ (w : A), w = w)
feat(library/defeq_simplifier): new simplifier that uses only definitional equalities 2016-02-13 18:52:25 +00:00			`λ (x y z w : A), q (q (q w))`
			`A → A → A → (∀ (w : A), q (q (q w)) = w)`
			`λ (x y z w : A), q (f (q (q x)) (q (q z)) (q w))`
			`∀ (x : A), A → (∀ (z w : A), q (f (q (q x)) (q (q z)) (q w)) = w)`
			`λ (x y z w : A), q (q (q w))`
			`A → A → A → (∀ (w : A), q (q (q w)) = w)`
			`λ (x y z w : A), w`
			`A → A → A → (∀ (w : A), w = w)`