From 135f5ff96b3fe2f1f32f1198dfaff879f9552fa5 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 24 Sep 2015 23:38:20 -0400
Subject: [PATCH] feat(library/init/quot.lean): declare calc subst rule for iff

---
 library/init/quot.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/library/init/quot.lean b/library/init/quot.lean
index c28104ace..97055225e 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -13,6 +13,10 @@ constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
 -- Remark: if we do not use propext here, then we would need a quot.lift for propositions.
 constant propext {a b : Prop} : (a ↔ b) → a = b
 
+-- iff can now be used to do substitutions in a calculation
+theorem iff_subst [subst] {a b : Prop} {P : Prop → Prop} (H₁ : a ↔ b) (H₂ : P a) : P b :=
+eq.subst (propext H₁) H₂
+
 namespace quot
   protected constant mk        : Π {A : Type}   [s : setoid A], A → quot s
   notation `⟦`:max a `⟧`:0 := quot.mk a