2015-11-04 21:53:12 -08:00
|
|
|
/- Basic rewriting with eq and lambda without congruence or conditionals -/
|
|
|
|
|
universe l
|
|
|
|
|
constant T : Type.{l}
|
|
|
|
|
constants (x y z : T) (f g h : T → T)
|
|
|
|
|
constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
|
|
|
|
|
|
|
|
|
|
attribute Hfxgy [simp]
|
|
|
|
|
#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
|
2015-11-06 21:02:04 -08:00
|
|
|
attribute Hgyhz [simp]
|
2015-11-04 21:53:12 -08:00
|
|
|
#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z
|
|
|
|
|
|
