Commit 2eda9022 authored by svenw's avatar svenw
Browse files

really the last push

parent d9161f72
......@@ -41,10 +41,19 @@ theory exampleInstantiationUsage : ur:?PLF =
q : tp ⟶ tp ⟶ tp ❙
ex5 : {a : tp} {b : tp}{c : tp } q a b ≡ a ⟶ p a ⟶ p (q a b) ❘
// fixs; rewrite h; simp; use h0❙
op : tp ⟶ tp ⟶ tp ❙
opassoc : {va : tp}{vb :tp }{vc : tp} op (op va vb) vc ≡ op va (op vb vc) ❙
ex5_1 : {a : tp} {b : tp}{c : tp } q a b ≡ a ⟶ p a ⟶ p (q a b) ❘
// fixs; symmetry in h; rewrite h in h0 ; use h0❙
ex6 : {x : tp }{y : tp}{P : tp ⟶ tp ⟶ tp ⟶ type} x ≡ y ⟶ P x y y ⟶ P x x y ❘ // fixs; rewrite h at 1 ; simp ; use h0 ❙
ex7 : {x : tp }{y : tp}{z : tp}{P : tp ⟶ tp ⟶ tp ⟶ type} x ≡ y ⟶ x ≡ z ⟶ P x y z ⟶ P x x x ❘
// fixs; rewrite h0 at 2; simp; rewrite h at 1; simp; use h1❙
ex7_1 : {x : tp }{y : tp}{z : tp}{P : tp ⟶ tp ⟶ tp ⟶ type} x ≡ y ⟶ x ≡ z ⟶ P x y z ⟶ P x x x ❘
// fixs; symmetry in h; symmetry in h0; rewrite h in h1 where (p := [u : tp] P x u z); simp in h1; rewrite h0 in h1 where (p := [u : tp] P x x u); simp in h1; use h1 ❘
// fixs; rewrite h in h1 where (p := [u : tp] P x u z); simp in h1; rewrite h0 in h1 where (p := [u : tp] P x x u); simp in h1; use h1❙
f : tp ⟶ type ❙
altcongr : {pp : tp ⟶ type }{ a : tp}{b : tp } a ≡ b ⟶ f a ⟶ pp b ❙
qq : tp ⟶ type ❙
ex8 : {u : tp}{v : tp} v ≡ u ⟶ f u ⟶ qq v ❘ // fixs; rewrite h using altcongr where (p := [x : tp] qq x ); use h0 ❙
ex8 : {a : tp}{b : tp}{c : tp}{d : tp} op (op (op a b) c) d ≡ op a (op b (op c d)) ❙
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment