22 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
22 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
23 (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf |
23 (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf |
24 | rew _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
24 | rew _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
25 (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) = |
25 (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) = |
26 Some (equal_intr_axm % B % A %% prf2 %% prf1) |
26 Some (equal_intr_axm % B % A %% prf2 %% prf1) |
|
27 |
|
28 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %% |
|
29 (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) % |
|
30 _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% |
|
31 ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
|
32 Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) |
|
33 |
|
34 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %% |
|
35 (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
|
36 (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) % |
|
37 _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %% |
|
38 ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
|
39 Some (tg %> B %% (equal_elim_axm %> A %> B %% |
|
40 (symmetric_axm % None % None %% prf1) %% prf2)) |
27 |
41 |
28 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
42 | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
29 (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
43 (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
30 (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %% |
44 (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %% |
31 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) = |
45 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) = |