From a07598a3eca71c320c99a8582243df5d7ebc22fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2015 13:19:52 -0800 Subject: [PATCH] feat(hott/init/logic): congr_fun was missing in the HoTT library, blast assumes it is part of the environment --- hott/init/logic.hlean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 069c08c500..2693ac89b7 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -65,6 +65,9 @@ eq.rec H₁ H₂ definition congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ := eq.subst H₁ (eq.subst H₂ rfl) +theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a := +eq.subst H (eq.refl (f a)) + theorem congr_arg {A B : Type} (a a' : A) (f : A → B) (Ha : a = a') : f a = f a' := eq.subst Ha rfl