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

chore(library/standard/piext): cleanup hcongr proof

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 19:08:53 +01:00
parent cb93d194ed
commit bd82f5e81c
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/standard/piext.lean
View file

@ -27,8 +27,8 @@ theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x}
theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'} theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
(Hff' : f == f') (Haa' : a == a') : f a == f' a' (Hff' : f == f') (Haa' : a == a') : f a == f' a'
:= have H : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from := have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
take B B' f f' e, hcongr1 a e, take B B' f f' e, hcongr1 a e,
@hsubst _ _ _ _ (fun (X : Type) (x : X), have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
∀ (B : A → Type) (B' : X → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' x) hsubst Haa' H1,
Haa' H B B' f f' Hff' H2 B B' f f' Hff'