From a7116b44c11559470e2d4f87ce86877face01034 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Oct 2020 05:39:25 -0700 Subject: [PATCH] test: add new subst tests --- tests/lean/run/subst.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/lean/run/subst.lean b/tests/lean/run/subst.lean index f30f77ce35..fd241a468f 100644 --- a/tests/lean/run/subst.lean +++ b/tests/lean/run/subst.lean @@ -17,6 +17,12 @@ h ▸ rfl theorem ex3 {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := h₂ ▸ h₁ +theorem ex3b {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := +h₂.symm ▸ h₁ + +theorem ex3c {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := +h₂.symm.symm ▸ h₁ + theorem ex4 {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := h₁ ▸ h₂