michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott/init/logic): congr_fun was missing in the HoTT library, blast assumes it is part of the environment

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-08 13:19:52 -08:00
parent 39019b6873
commit a07598a3ec
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/init/logic.hlean
View file

@ -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