proof of $\perp$. This would allow us to assume a term `negatedConjecture`: `Prf(¬ conjecture)` and then, in turn, provide the steps of the previous proof encoding as subproofs. `¬I` can then be used to map the term of type `Prf(¬ conjecture) → Prf⊥` to a term of type `Prf(¬ ¬ conjecture)`. Proving the conjecture based on this is then a simple instantiation of `npp`. This way, not only the inference steps but also the approach of proving the conjecture by refutation would be verified. In the future development of the implementation, this proof encoding will thus be adopted.

## 7.3 Future work.

### 7.3.1 Correctness of the encoding

Proving the soundness of the encoding proposed in Section 3.2 is challenging and must be addressed in future work. A common approach involves proving both termination and confluence, and then arguing that these properties ensure the existence of a normal form that corresponds to a proof in natural deduction [6]. However, proving termination is difficult, though research on proof termination for super-consistent systems may present a promising option [32]. Existing proofs for related systems and alternative encoding approaches could also offer solutions. For instance, [35] suggests a new computational approach to encoding systems in Dedukti, resulting in encodings for which correctness is easier to prove by design. Another method for HOL is to encode it following the pure type system formalism. Minimal constructive HOL can be expressed as a pure type system, as proposed in [4], the encoding of which is shown to be sound in [28, 4]. The Holide project demonstrates an alternative encoding of HOL [5], differing from the theory U encoding by using equality as the primitive connective rather than implication and universal quantification.

### 7.3.2 Planned Extensions of the encoding.

The extended calculus EP of Leo-III comprises over 30 inference rules in total and the encoding presented here will have to be extended to this full set of rules. Apart from that, two restrictions were imposed on the encoding presented herein that will be lifted in future work. The theoretical encoding will therefore be extended in three steps:

I) Extension of the encoding to the full (extended) calculus EP.

II) Verification of the clausification steps, including skolemization.

III) The extension of the type system and inference rules with rank 1 polymorphism.

This will then be the theoretical foundation based on which the extensions of existing tools will be carried out to automatically verify HOL proofs in the Dedukti framework:

IV) The full implementation of automated proof encoding of Leo-III.

V) The extension of the tool GDV for HOL.

Fig. 18 sets the steps representing the theoretical work (I - III) necessary to automatize the encodings of Leo-III proofs into the context of the reasoning process of the Leo-III system and illustrates how the implementation of an automated encoding (IV) will result in verifiable proofs that can in turn be used to extend GDV-LP (V).

**I.** The specific requirements of the remaining inference rules have to be analyzed in a similar fashion as the ones presented herein and the developed verification and encoding strategies will have to be adapted accordingly. Furthermore, a representation of the choice operator present in Leo-III has to be added to the Lambdapi theory in order to encode the choice related rules. This will extend the work presented here to a complete foundational encoding of monomorphic HOL problems and proofs with an restriction to CNF.
<figure><img src="image_10.png" /><figcaption>Figure 18: Next Steps in the Context of the Interacting Systems. The colored dotted lines divide the illustrated processes into the different systems: Leo-III is light blue, the Lambdapi extension is turquoise, GDP-LP is green and red signifies other ATP systems. The entities these systems operate on are given with a black backdrop and black arrows indicate steps of the reasoning process. The next steps are indicated by their respective numbers in black circles and placed on the arrow of their associated processes. Turquoise labels specify which steps are being encoded.</figcaption></figure>

II. The verification approaches used in Dedukti aim at proving that derived formulas are logical consequences of their parents, which does not hold for skolemization, making the application of alternative strategies necessary. This problem is also encountered in FOL reasoning and has likewise come up in the implementation of some of the previously mentioned FOL tools [40, 66, 22]. SKonverto<fnref n="9" /> is a tool designed to derive a Dedukti proof without Skolem terms from a FOL TPTP proof that involved skolemization. There is, however, a lack of currently available strategies for HOL in this respect, and the development, assessment, and implementation of such techniques will have merit beyond the scope of this project. The extension of SKonverto offers a promising prospect.

III. A further challenge is represented by the encoding of the polymorphism of Leo-III. Handling the specific restrictions it is governed by (type quantification only ranges over monomorphic types and can only be used at prenex position, type variables only range over monomorphic types and only monomorphic types are allowed as arguments to type applications [65]) will entail two steps: First, the current theory has to be extended with operators that quantify, apply and abstract over the monomorphic and polymorphic types. This has to be tailored to the specific restrictions to accurately represent the type system of Leo-III. Second, polymorphic types have to be unified to ensure their compatibility before rule applications. This additional step is governed by its own set of type unification rules, which will likewise have to be encoded, proven and included in the Lambdapi output.

IV. Together these objectives will provide the encodings and strategies necessary to produce verifiable Lambdapi proofs. The encoding will be automatized as an open source Lambdapi extension of Leo-III.

V. Upon the completion of the automated encoding, Leo-III can be used to verify proofs of other HOL systems outputting TSTP certificates. This can be achieved through the extension of GDV-LP [66] with the option to invoke Leo-III as a trusted prover.

<footnote n="9">⁹https://github.com/Deducteam/SKonverto</footnote>
References

[1] P. B. Andrews. General models and extensionality. *The Journal of Symbolic Logic*, 37(2):395–397, 1972.

[2] P. B. Andrews. General models, descriptions, and choice in type theory. *J. Symb. Log.*, 37(2):385–394, 1972.

[3] P. B. Andrews. *An introduction to mathematical logic and type theory: to truth through proof*, volume 27. Springer Science & Business Media, 2013.

[4] A. Assaf. *A framework for defining computational higher-order logics*. PhD thesis, École polytechnique, 2015.

[5] A. Assaf and G. Burel. Translating HOL to dedukti. In C. Kaliszyk and A. Paskevich, editors, *Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015*, volume 186 of *EPTCS*, pages 74–88, 2015.

[6] A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Dedukti: a logical framework based on the λΠ-calculus modulo theory. *CoRR*, abs/2311.07185, 2023.

[7] F. Baader and T. Nipkow. *Term rewriting and all that*. Cambridge university press, 1998.

[8] H. Barendregt. Introduction to generalized type systems. *J. Funct. Program.*, 1(2):125–154, 1991.

[9] H. P. Barendregt, W. Dekkers, and R. Statman. *Lambda Calculus with Types*. Perspectives in logic. Cambridge University Press, 2013.

[10] C. Benzmüller. *Equality and extensionality in automated higher order theorem proving*. PhD thesis, Saarland University, Saarbrücken, Germany, 1999.

[11] C. Benzmüller, C. E. Brown, and M. Kohlhase. Higher-order semantics and extensionality. *J. Symb. Log.*, 69(4):1027–1088, 2004.

[12] C. Benzmüller, C. E. Brown, and M. Kohlhase. Cut-simulation and impredicativity. *Log. Methods Comput. Sci.*, 5(1), 2009.

[13] C. Benzmüller and D. Miller. Automation of higher-order logic. In J. H. Siekmann, editor, *Computational Logic*, volume 9 of *Handbook of the History of Logic*, pages 215–254. Elsevier, 2014.

[14] C. Benzmüller and P. Andrews. Church's Type Theory. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Spring 2024 edition, 2024.

[15] P. Blackburn, J. F. van Benthem, and F. Wolter. *Handbook of modal logic*. Elsevier, 2006.

[16] B. Blanchet. Modeling and verifying security protocols with the applied pi calculus and proverif. *Found. Trends Priv. Secur.*, 1(1-2):1–135, 2016.

[17] F. Blanqui. Type safety of rewrite rules in dependent types. In Z. M. Ariola, editor, *5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)*, volume 167 of *LIPIcs*, pages 13:1–13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[18] F. Blanqui, G. Dowek, É. Grienenberger, G. Hondet, and F. Thiré. A modular construction of type theories. *Log. Methods Comput. Sci.*, 19(1), 2023.

[19] S. Bobzien. Ancient Logic. In E. N. Zalta, editor, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Summer 2020 edition, 2020.
[20] M. Boespflug and G. Burel. Coqine: Translating the calculus of inductive constructions into the λΠ-calculus modulo. In D. Pichardie and T. Weber, editors, *Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012*, Manchester, UK, June 30, 2012, volume 878 of *CEUR Workshop Proceedings*, pages 44–50. CEUR-WS.org, 2012.

[21] G. Burel. Experimenting with deduction modulo. In N. S. Bjørner and V. Sofronie-Stokkermans, editors, *Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings*, volume 6803 of *Lecture Notes in Computer Science*, pages 162–176. Springer, 2011.

[22] G. Burel. A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo. In J. C. Blanchette and J. Urban, editors, *Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013*, volume 14 of *EPiC Series in Computing*, pages 43–57. EasyChair, 2013.

[23] G. Bury. *Integrating rewriting, tableau and superposition into SMT*. (Intégrer la réecriture, la méthode des tableaux et la superposition dans les solveurs SMT). PhD thesis, Sorbonne Paris Cité, France, 2019.

[24] G. Cantor. Über eine elementare frage der mannigfaltigkeitslehre, jahresbericht der dmv (vol. 1, pp. 75–78). references to cantor (1932). *English trans. in Ewald (1996)*, 2:278–280, 1892.

[25] A. Church. A formulation of the simple theory of types. *J. Symb. Log.*, 5(2):56–68, 1940.

[26] A. Coltellacci, S. Merz, and G. Dowek. Reconstruction of SMT proofs with lambdapi. In G. Reger and Y. Zohar, editors, *Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024*, volume 3725 of *CEUR Workshop Proceedings*, pages 13–23. CEUR-WS.org, 2024.

[27] T. Coquand and G. P. Huet. The calculus of constructions. *Inf. Comput.*, 76(2/3):95–120, 1988.

[28] D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In S. R. D. Rocca, editor, *Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings*, volume 4583 of *Lecture Notes in Computer Science*, pages 102–117. Springer, 2007.

[29] H. B. Curry. Functionality in combinatory logic. *Proceedings of the National Academy of Sciences*, 20(11):584–590, 1934.

[30] N. G. De Bruijn. The mathematical language automath, its usage, and some of its extensions. In *Studies in Logic and the Foundations of Mathematics*, volume 133, pages 73–100. Elsevier, 1994.

[31] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant. Zenon modulo: When achilles outruns the tortoise using deduction modulo. In K. L. McMillan, A. Middeldorp, and A. Voronkov, editors, *Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings*, volume 8312 of *Lecture Notes in Computer Science*, pages 274–290. Springer, 2013.

[32] G. Dowek. Models and termination of proof reduction in the lambda pi-calculus modulo theory. In I. Chatzigiannakis, P. Indyk, F. Kuhn, and A. Muscholl, editors, *44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland*, volume 80 of *LIPIcs*, pages 109:1–109:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.

[33] G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. *J. Autom. Reason.*, 31(1):33–72, 2003.

[34] G. Dowek and B. Werner. Proof normalization modulo. *J. Symb. Log.*, 68(4):1289–1316, 2003.
[35] T. Felicissimo. Adequate and computational encodings in the logical framework dedukti. In A. P. Felty, editor, *7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel*, volume 228 of LIPIcs, pages 25:1–25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[36] H. Freudenthal. Zur intuitionistischen deutung logischer formeln. *Compositio mathematica*, 4:112-116, 1937.

[37] H. Ganzinger and C. Benzmüller. Extensional higher-order paramodulation and rue-resolution. In *Automated Deduction—CADE-16: 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings 16*, pages 399–413. Springer, 1999.

[38] G. Gentzen. Untersuchungen über das logische schließen. ii. *Mathematische zeitschrift*, 39, 1935.

[39] K. Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme i. *Monatshefte für mathematik und physik*, 38:173–198, 1931.

[40] M. Y. E. Haddad, G. Burel, and F. Blanqui. EKSTRAKTO A tool to reconstruct dedukti proofs from TSTP files (extended abstract). In G. Reis and H. Barbosa, editors, *Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019*, volume 301 of EPTCS, pages 27–35, 2019.

[41] R. Harper, F. Honsell, and G. D. Plotkin. A framework for defining logics. In *Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987*, pages 194–204. IEEE Computer Society, 1987.

[42] L. Henkin. Completeness in the theory of types. *J. Symb. Log.*, 15(2):81–91, 1950.

[43] L. Horsten. Philosophy of Mathematics. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Winter 2023 edition, 2023.

[44] W. A. Howard et al. The formulae-as-types notion of construction. *To HB Curry: essays on combinatory logic, lambda calculus and formalism*, 44:479–490, 1980.

[45] G. P. Huet. A unification algorithm for typed lambda-calculus. *Theor. Comput. Sci.*, 1(1):27–57, 1975.

[46] M. Janowicz, L. Ochnio, L. J. Chmielewski, and A. Orlowski. Application of automated theorem-proving to philosophical thought: Spinoza's ethics. In *Information Science and Applications 2017: ICISA 2017 8*, pages 512–518. Springer, 2017.

[47] J. W. Klop, V. Van Oostrom, and F. Van Raamsdonk. Combinatory reduction systems: introduction and survey. *Theoretical computer science*, 121(1-2):279–308, 1993.

[48] M. Kohlhaase. *A mechanization of sorted higher-order logic based on the resolution principle*. PhD thesis, Saarland University, Saarbrücken, Germany, 1994.

[49] L. Kovács and A. Voronkov. First-order theorem proving and vampire. In N. Sharygina and H. Veith, editors, *Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings*, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer, 2013.

[50] G. W. Leibniz and G. W. Leibniz. *Discourse on Metaphysics: 1686*. Springer, 1989.

[51] W. McCune. Solution of the robbins problem. *J. Autom. Reason.*, 19(3):263–276, 1997.

[52] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. *J. Log. Comput.*, 1(4):497–536, 1991.
[53] J. Moschovakis. Intuitionistic Logic. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Summer 2023 edition, 2023.

[54] M. Odersky, P. Altherr, V. Cremet, B. Emir, S. Maneth, S. Micheloud, N. Mihaylov, M. Schinz, E. Stenman, and M. Zenger. An overview of the scala programming language. 2004.

[55] J. Otten. Mleancop: A connection prover for first-order modal logic. In S. Demri, D. Kapur, and C. Weidenbach, editors, *Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings*, volume 8562 of *Lecture Notes in Computer Science*, pages 269-276. Springer, 2014.

[56] F. J. Pelletier and A. Hazen. Natural Deduction Systems in Logic. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Spring 2024 edition, 2024.

[57] F. Portoraro. Automated Reasoning. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Summer 2023 edition, 2023.

[58] M. Rathjen and W. Sieg. Proof Theory. In E. N. Zalta and U. Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Spring 2024 edition, 2024.

[59] G. Robinson and L. Wos. Paramodulation and theorem-proving in first-order theories with equality. In *Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970*, pages 298-313. Springer, 1983.

[60] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965.

[61] S. Schulz. E - a brainiac theorem prover. AI Commun., 15(2-3):111-126, 2002.

[62] A. Steen. *Extensional paramodulation for higher-order logic and its effective implementation Leo-III*. PhD thesis, Free University of Berlin, Dahlem, Germany, 2018.

[63] A. Steen and C. Benzmüller. Extensional higher-order paramodulation in leo-iii. J. Autom. Reason., 65(6):775-807, 2021.

[64] A. Steen, G. Sutcliffe, T. Scholl, and C. Benzmüller. Solving modal logic problems by translation to higher-order logic. In A. Herzig, J. Luo, and P. Pardo, editors, *Logic and Argumentation - 5th International Conference, CLAR 2023, Hangzhou, China, September 10-12, 2023, Proceedings*, volume 14156 of *Lecture Notes in Computer Science*, pages 25-43. Springer, 2023.

[65] A. Steen, M. Wisniewski, and C. Benzmüller. Going polymorphic - TH1 reasoning for leo-iii. In T. Eiter, D. Sands, G. Sutcliffe, and A. Voronkov, editors, *IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017*, volume 1 of *Kalpa Publications in Computing*, pages 100-112. EasyChair, 2017.

[66] G. Sutcliffe. Semantic derivation verification: Techniques and implementation. Int. J. Artif. Intell. Tools, 15(6):1053-1070, 2006.

[67] G. Sutcliffe. The TPTP World - Infrastructure for Automated Reasoning. In E. Clarke and A. Voronkov, editors, *Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning*, number 6355 in Lecture Notes in Artificial Intelligence, pages 1-12. Springer-Verlag, 2010.

[68] G. Sutcliffe. The CADE ATP System Competition - CASC. AI Magazine, 37(2):99-101, 2016.
[69] G. Sutcliffe. The Logic Languages of the TPTP World. *Logic Journal of the IGPL*, 2022.

[70] M. Taprogge. Leo-iii-lp, 2024. https://zenodo.org/records/13889978.

[71] M. Taprogge and A. Steen. Flexible automation of quantified multi-modal logics with interactions. In *German Conference on Artificial Intelligence (Künstliche Intelligenz)*, pages 215–230. Springer, 2023.

[72] P. Wadler. Propositions as types. *Communications of the ACM*, 58(12):75–84, 2015.

[73] A. N. Whitehead and B. Russell. *Principia mathematica to* 56, volume 2. Cambridge University Press, 1997.
A Construction Rules

// head symbol ∧

2

3 opaque symbol c∧r a b c : ( Prf b → Prf c ) → Prf ( a ∧ b ) → Prf ( a ∧ c ) :=

4 begin

5 assume a b c h1 h2;

6 have H1 : Prf a

7 {refine ∧E1 a b h2};

8 have H2 : Prf c

9 {refine h1 (∧Er a b h2)};

10 refine ∧I a c H1 H2;

11 end;

12

13 opaque symbol c∧l a b c : ( Prf a → Prf c ) → Prf ( a ∧ b ) → Prf ( c ∧ b ) :=

14 begin

15 assume a b c h1 h2;

16 have H1 : Prf b

17 {refine ∧Er a b h2};

18 have H2 : Prf c

19 {refine h1 (∧E1 a b h2)};

20 refine ∧I c b H2 H1;

21 end;

22

23

// head symbol ∨

25

26 opaque symbol c∨r a b c : ( Prf b → Prf c ) → Prf ( a ∨ b ) → Prf ( a ∨ c ) :=

27 begin

28 assume a b c h1 h2 b1 h3 h4;

29 have H1: Prf b → Prf b1

30 {assume h5;

31 refine h4 (h1 h5)};

32 refine ∨E a b b1 h3 H1 h2;

33 end;

34

35 opaque symbol c∨l a b c : ( Prf a → Prf c ) → Prf ( a ∨ b ) → Prf ( c ∨ b ) :=

36 begin

37 assume a b c h1 h2 b1 h3 h4;

38 have H1: Prf a → Prf b1

39 {assume h5;

40 refine h3 (h1 h5)};

41 refine ∨E a b b1 H1 h4 h2;

42 end;

43

44

// head symbol ⇒

46

47 opaque symbol c⇒ a b c : ( Prf b → Prf c ) → Prf ( a ⇒ b ) → Prf ( a ⇒ c ) :=

48 begin

49 assume a b c h1 h2 h3;

50 refine h1 (h2 h3)

51 end;

52

53

// head symbol ¬

55
```
opaque symbol c¬ x y : ((Prf y) → (Prf x)) → Prf(¬ x) → Prf (¬ y) :=
begin
  assume x y h1 h2 h3 b;
  refine h2 (h1 h3) b;
end;

// head symbol =
opaque symbol eqTrainsitivity [T] (a b c : El T) : Prf(a = b) → Prf(b = c) → Prf
(a = c) :=
begin
  assume T a b c h1 h2 g h3T;
  have H1: Prf(g b)
    {refine h1 g h3T};
  refine h2 g H1
end;

opaque symbol c=1 [T] a b c (f g : Prop → El T) : (Prf a → Prf c) → (Prf c → Prf
a) → Prf((f a) = (g b)) → Prf((f c) = (g b)):=
begin
  assume T a b c f g h1 h2 h3;
  have H1 : Prf (c = a)
    {refine propExt c a h2 h1};
  have H2 : Prf ((f c) = (f a))
    {refine =def [o] c a H1 (λ z, (f z) = (f a)) (=ref [T] (f a))};
  refine eqTrainsitivity [T] (f c) (f a) (g b) H2 h3;
end;

opaque symbol c=r [T] a b c (f g : Prop → El T) : (Prf b → Prf c) → (Prf c → Prf
b) → Prf((f a) = (g b)) → Prf((f a) = (g c)):=
begin
  assume T a b c f g h1 h2 h3;
  have H1 : Prf (b = c)
    {refine propExt b c h1 h2};
  have H2 : Prf ((g b) = (g c))
    {refine =def [o] b c H1 (λ z, (g z) = (g c)) (=ref [T] (g c))};
  refine eqTrainsitivity [T] (f a) (g b) (g c) h3 H2;
  proofterm;
end;

// Head symbol ∀
opaque symbol c∀ [T] (x : El T) a b : (Prf a → Prf b) → Prf(∀(λ x : El T, a) ) →
Prf(∀(λ x : El T, b) ) :=
begin
  assume T x a b h1 h2 h3;
  refine h1 (h2 x);
end;

// Head symbol ∃
opaque symbol c∃ [T] (x : El T) a b : (Prf a → Prf b) → Prf(∃(λ x : El T, a) ) →
Prf(∃(λ x : El T, b) ) :=
begin
```
108 simplify;
109 assume T x a b h1 h2 b1 h3;
110 have H1: Prf b
111 {refine h2 b (λ x , h1)};
112 refine h3 x H1
113 end;
114
115
116 // Head symbol λ
117
118 opaque symbol cλ q a b : (Prf a → Prf b) → (Prf b → Prf a) → Prf((λ x : El o, q x)a) → Prf((λ x : El o, q x)b) :=
119 begin
120 assume q a b h1 h2 h3;
121 refine =def b a (propExt b a h2 h1) q h3;
122 end;

Note that the rules here are proven using the rewrite rules defining the connectives. The reason for this is that these rules are only used in the encodings that do not use the *rewrite* tactic and therefore the rewrite rules can be safely imported into the files containing the proof verification rather than being provided in an extra file like correctness.lp.
## B Accessory Rules for Transforming to Equational Literals and back

```
opaque symbol posPropNegEq_eq x: (Prf (x = (¬ ((¬ x) = T)))):=
```

```
begin
```

```
assume x;
```

```
refine propExt x (¬ ((¬ x) = T)) _ _
```

```
{assume h1;
```

```
have H1: Prf((¬ x) = T) → Prf ⊥
```

```
{assume h2;
```

```
refine ¬E x h1 ((=def [o] (¬ x) T h2 (λ z, z) TI));
```

```
refine ¬I ((¬ x) = T) H1}
```

```
{assume h1;
```

```
refine ∨E x (¬ x) x _ _ (em x)
```

```
{assume h2;
```

```
refine h2}
```

```
{assume h2;
```

```
have H1: Prf((¬ x) = T)
```

```
{refine propExt (¬ x) T _ _
```

```
{assume h3;
```

```
refine TI}
```

```
{assume h3;
```

```
refine h2}};
```

```
refine ⊥E x (¬E ((¬ x) = T) H1 h1)}
```

```
end;
```

```
begin
```

```
opaque symbol negPropPosEq_eq x: (Prf ((¬ x) = ((¬ x) = T))):=
```

```
begin
```

```
assume x;
```

```
refine propExt (¬ x) ((¬ x) = T) _ _
```

```
{assume h1;
```

```
refine propExt (¬ x) T _ _
```

```
{assume h2;
```

```
refine TI}
```

```
{assume h2;
```

```
refine h1}}
```

```
{assume h1;
```

```
have H1: Prf((¬ x) = T) → Prf(¬ x)
```

```
{assume h2;
```

```
refine (=def [o] (¬ x) T h2 (λ z, z) TI);
```

```
refine H1 h1}
```

```
end;
```

```
begin
```

```
opaque symbol negPropNegEq_eq x: (Prf ((¬ x) = (¬ (x = T)))):=
```

```
begin
```

```
assume x;
```

```
refine propExt (¬ x) (¬ (x = T)) _ _
```

```
{assume h1;
```

```
have H1: Prf(x = T) → Prf ⊥
```

```
{assume h2;
```

```
refine ¬E x (=def [o] x T h2 (λ z, z) TI) h1;
```

```
refine ¬I (x = T) H1}
```

```
{assume h1;
```

```
refine ¬I x _;
```

```
assume h2;
```

```
have H1: Prf(x = T)
```
54 {refine propExt x ⊤ _ _
55 {assume h3;
56   refine ⊤I}
57 {assume h3;
58   refine h2}};
59 refine ¬E (x = ⊤) H1 h1}
60 end;
61
62 opaque symbol topPosProp_eq x: (Prf ((⊤ = x) = x)):=
63 begin
64   assume x;
65   refine propExt (⊤ = x) x _ _
66   {assume h1;
67     have H1 : Prf x → Prf x
68       {assume h2;
69       refine h2};
70     refine (⇒E ⊤ x (=def ⊤ x h1 (λ z, z ⇒ x) (⇒I x x H1))) ⊤I}
71   {assume h1;
72   refine propExt ⊤ x _ _
73     {assume h2;
74       refine h1}
75     {assume h2;
76       refine ⊤I}}
77 end;
78
79 opaque symbol botNegProp_eq x: (Prf ((⊥ = x) = (¬ x))):=
80 begin
81   assume x;
82   refine propExt (⊥ = x) (¬ x) _ _
83   {assume h1;
84     have H1 : Prf x → Prf x
85       {assume h2;
86       refine h2};
87     refine ¬I x (⇒E x ⊥ (=def ⊥ x h1 (λ z, x ⇒ z) (⇒I x x H1)))}
88   {assume h1;
89   refine propExt ⊥ x _ _
90     {assume h2;
91       refine ⊥E x h2}
92     {assume h2;
93       refine ¬E x h2 h1}}
94 end;
C Simplification Rules

First, the proofs of simplification rules will be explained using (Simp7) as an example, then the remaining rules will be defined.

Generally, the proof of the equality literals will follow the same pattern: We will first assume the variables of the respective encoding and then use the Lambdapi-axiom `propExt`, which maps the proofs of a bidirectional implication of two terms to a proof of their equality. Both directions of the implication will then be shown in two subproofs. In the case of (Simp7), which allows us to omit $⊥$ from a disjunction `((s ∨ ⊥) → s)$`, the encoding can be proven as follows:

```
1 opaque symbol simp7_eq x: (Prf (x = (x ∨ ⊥))):=
2 begin
3   assume x;
4   refine propExt x (x ∨ ⊥) _ _
5   {assume h1;
6   refine ∨I1 x ⊥ h1}
7   {assume h1;
8   refine ∨E x ⊥ x _ _ h1
9   {assume h2;
10   refine h2}
11   {assume h2;
12   refine ⊥E x h2}}
13 end;
```

The two subproofs we need to provide here are for `Prf x → Prf (x ∨ ⊥)` and the reverse direction, `Prf (x ∨ ⊥) → Prf x`. To prove the former, we assume `h1`: `Prf x` (line 5), which we can use to prove the new focused goal `Prf (x ∨ ⊥)` using the introduction rule `∨I1` (line 6). In the second subproof, we assume `h1`: `Prf (x ∨ ⊥)` (line 7) and use the elimination rule `∀E` and two subproofs demonstrating that `x` follows from both sides of the disjunction individually, to provide a term of type `Prf x` (line 8). For the left-hand side, we need to prove `Prf x → Prf x`, which can be achieved by simply assuming `h2`: `Prf x` and refining with it (lines 9 and 10). For the right-hand side, the assumption of `h2`: `Prf ⊥` can be mapped to an arbitrary proof using `⊥E`. An instantiation with `x` thus yields the desired proof (lines 11 and 12).

The proofs of the remaining simplification rules follow the same pattern:

```
1 opaque symbol simp1_eq x: (Prf (x = (x ∨ x))):=
2 begin
3   assume x;
4   refine propExt x (x ∨ x) _ _
5   {assume h2;
6   refine ∨I1 x x h2}
7   {assume h1;
8   refine ∨E x x x _ _ h1
9   {assume h2;
10   refine h2}
11   {assume h2;
12   refine h2}}
13 end;
14
15 opaque symbol simp2_eq x: (Prf (x = (x ∧ x))):=
16 begin
17   assume x;
18   refine propExt x (x ∧ x) _ _
```
19 {assume h1;
20 refine $\wedge I x x h1 h1$
21 {assume h1;
22 refine $\wedge E1 x x h1$
23 end;
24
25 opaque symbol simp3_eq x: (Prf ($\vdash$ = (($\neg$ x) $\lor$ x))):=
26 begin
27 assume x;
28 refine propExt $\vdash$ (($\neg$ x) $\lor$ x) _ _
29 {assume h2;
30 have em_sym: Prf($\neg$ x $\lor$ x)
31 {refine $\lor E$ x ($\neg$ x) ($\neg$ x $\lor$ x) _ _ (em x)
32 {assume h3;
33 refine $\lor I r$ ($\neg$ x) x h3}
34 {assume h3;
35 refine $\lor I l$ ($\neg$ x) x h3}};
36 refine em_sym}
37 {assume h1;
38 refine $\vdash I$
39 end;
40
41 opaque symbol simp4_eq x: (Prf ($\vdash$ = (($\neg$ x) $\land$ x))):=
42 begin
43 assume x;
44 refine propExt $\vdash$ (($\neg$ x) $\land$ x) _ _
45 {assume h1;
46 refine $\vdash E$ ($\neg$ x $\land$ x) h1}
47 {assume h1;
48 refine $\neg E$ x _ _
49 {refine $\wedge Er$ ($\neg$ x) x h1}
50 {refine $\wedge E1$ ($\neg$ x) x h1}}
51 end;
52
53 opaque symbol simp5_eq x: (Prf ($\vdash$ = ($x \lor \top$))):=
54 begin
55 assume x;
56 refine propExt $\vdash$ ($x \lor \top$) _ _
57 {assume h2;
58 refine $\lor I r$ x $\vdash$ h2}
59 {assume h1;
60 refine $\vdash I$
61 end;
62
63 opaque symbol simp6_eq x: (Prf ($x$ = ($x \land \top$))):=
64 begin
65 assume x;
66 refine propExt x ($x \land \top$) _ _
67 {assume h1;
68 refine $\wedge I$ x $\vdash$ h1 $\vdash I$
69 {assume h1;
70 refine $\wedge E1$ x $\vdash$ h1}
71 end;
72
73 opaque symbol simp8_eq x: (Prf ($\vdash$ = ($x \land \bot$))):=
74 begin
75 assume x;
refine propExt ⊥ (x ∧ ⊥) _ _
{assume h1;
  type ⊥E x h1;
  refine ∧I x ⊥ (⊥E x h1) h1}
{assume h1;
  refine ∧Er x ⊥ h1}
end;

opaque symbol simp9_eq T x: (Prf (⊤ = (x = x))):=
begin
  assume T x;
  refine propExt ⊤ (x = x) _ _
    {assume h1;
      refine =ref [T] x}
    {assume h1;
      refine ⊤I}
end;

opaque symbol simp10_eq T x: (Prf (⊥ = (¬ (x = x))):=
begin
  assume T x;
  refine propExt ⊥ (¬ (x = x)) _ _
    {assume h1;
      refine ⊥E (¬ (x = x)) h1}
    {assume h1;
      have H1: Prf (x = x) → Prf ⊥
        {assume h2;
          refine ¬E (x = x) h2 h1};
      refine H1 (=ref [T] x)}
end;

opaque symbol simp11_eq x: (Prf (x = (x = ⊤))):=
begin
  assume x;
  refine propExt x (x = ⊤) _ _
    {assume h1;
      refine propExt x ⊤ _ _
        {assume h2;
          refine ⊤I}
        {assume h2;
          refine h1}}
    {assume h1;
      refine (=def [o] x ⊤ h1 (λ z: Prop, z)) ⊤I}
end;

opaque symbol simp12_eq x: (Prf ((¬ x) = (¬(x = ⊤)))):=
begin
  assume x;
  refine propExt (¬ x) (¬(x = ⊤)) _ _
    {assume h1;
      have H1: Prf(x = ⊤) → Prf ⊥
        {assume h2;
          have H1_1: Prf x
            {refine =def [o] x ⊤ h2 (λ z: Prop, z) ⊤I};
          refine ¬E x H1_1 h1};
      refine ¬I (x = ⊤) H1}
    {assume h1;
      refine =ref [T] x}
end;
have H1: Prf x → Prf ⊥
{assume h2;
refine ¬E (x = T) h1;
refine propExt x T
{assume h3;
refine TI;
{assume h3;
refine h2}};
refine ¬I x H1}
end;

opaque symbol simp15_eq: (Prf (T = (¬⊥))):=
begin
refine propExt T (¬⊥) _
{assume h1;
have H1: Prf ⊥ → Prf ⊥
{assume h2;
refine h2};
refine ¬I ⊥ H1}
{assume h1;
refine TI}
end;

opaque symbol simp16_eq: (Prf (⊥ = (¬T))):=
begin
refine propExt ⊥ (¬T) _
{assume h1;
refine ⊥E (¬T) h1}
{assume h1;
refine ¬E T TI h1}
end;

opaque symbol simp17_eq x: (Prf (x = (¬¬x))):=
begin
assume x;
refine propExt x (¬¬x) _
{assume h1;
have H1: Prf(¬x) → Prf ⊥
{assume h2;
refine ¬E x h1 h2};
refine ¬I (¬x) H1}
{assume h1;
refine npp x h1}
end;
# D Calculus Rules

## D.1 Functional Extensionality

```
1 opaque symbol PFE [T] [S] (f : (E1 (S ~ T))) (g : (E1 (S ~ T))) (x : (E1 S)): ((
   Prf (f = g)) → (Prf ((f x) = (g x)))) :=
2 begin
3   assume T S f g x h;
4   refine =def [(S ~ T)] f g h (λ y, (y x) = (g x)) (=ref [T] (g x))
5 end;
```

To prove the implication of `(f x) = (g x)` by `f = g`, `h: Prf(f = g)` is assumed and used to prove `(f x) = (g x)` through the use of `=def`, the instantiation of which results in the type `Prf ((g x) = (g x)) → Prf ((f x) = (g x))`. To this term, we can apply the instantiation of `=ref`, which proves `(g x) = (g x)` (line 4).

## D.2 Boolean Extensionality

Boolean Extensionality requires two proof terms representing the possible results for both (PBE), which is applied to positive equational literals, and (NBE), which is applied to negative ones. (PBE). The first encoding is defined as:

```
1 opaque symbol PBE_r x y: Prf(x = y) → Prf(x ∨ (¬ y)):=
2 begin
3   assume x y h;
4   refine =def [o] x y h (λ z, z ∨ (¬ y) (em y));
5 end;
```

First, the variables `x` and `y` as well as the hypothesis `h1: Prf (x = y)` are assumed (line 3), leaving `Prf (x ∨ (¬ y))` as the focused goal. A term of that type is provided by first applying `x`, `y`, `h` and the anonymous function `(λ z, z ∨ (¬ y))` to `=def`, which results in a term of type `Prf (y ∨ (¬ y)) → Prf (x ∨ (¬ y))`. The application of an instantiated version of the Lambdapi-axiom encoding the principle of the excluded middle, `em y` with type `Prf (y ∨ (¬ y))` therefore results in the required proof-term. The proof of the second rule is defined as follows.

```
1 opaque symbol PBE_l x y: Prf(x = y) → Prf((¬ x) ∨ y):=
2 begin
3   assume x y h;
4   have em_sym: Prf(¬ y ∨ y)
      {refine ∨E y (¬ y) (¬ y ∨ y) _ _ (em y)
         {assume h2;
          refine ∨Ir (¬ y) y h2}
         {assume h2;
          refine ∨I1 (¬ y) y h2}};
5   refine =def [o] x y h (λ z, (¬ z ∨ y) em_sym;
6
7
8
9
10
11 end;
```

The proof is analogous, the only difference is that we here require an additional step to show a permuted version of `em` (lines 4 to 9). This can be proven using the introduction and elimination rules of ∨ analogously to the proof provided in Sect. 4.3.3.
(NBE). The first version of the rule is defined as follows.

```
1 opaque symbol NBE_p x y: Prf(¬(x = y)) → Prf(x ∨ y):=
2 begin
3   assume x y h1;
4   refine ∨E x (¬ x) (x ∨ y) _ _ (em x)
5   {assume h2;
6    refine ∨I1 x y h2}
7   {assume h2;
8    have H1: Prf y
9     {have H2: Prf (¬ y) → Prf ⊥
10      {assume h3;
11       have H3: Prf x → Prf y
12        {assume h4;
13         refine ⊥E y (¬E x h4 h2)};
14        have H4: Prf y → Prf x
15        {assume h4;
16         refine ⊥E x (¬E y h4 h3)};
17         refine ¬E (x = y) (propExt x y H3 H4) h1};
18        refine npp (y) (¬I (¬ y) H2)};
19       refine ∨Ir x y H1};
20 end;
```

After assuming `x`, `y` and `h1`: `Prf(¬(x = y))`, the focused goal we are left with is `Prf(x ∨ y)`. We will follow a case distinction to construct a proof: We show in two subproofs that both `x` and `¬ x` imply `(x ∨ y)`. `∀E` can then be used to map these two proofs to `Prf(x ∨ ¬ x) → Prf(x ∨ y)`. Applying the instantiation of the Lambdapi-axiom `em` with `x`, resulting in a term of type `Prf(x ∨ ¬ x)`, then yields the desired proof-term. This is the `refine` step in line 4. The first subproof (lines 5-6) assumes `h2`: `Prf x` and then shows `Prf(x ∨ y)`, once more using the introduction rule of `∨` (line 7). For the second subproof we assume `h2`: `Prf(¬ x)` (line 8) and then need to show `Prf(x ∨ y)`. The idea we will follow to do so is to use the proof of the inequality of `x` and `y` provided by `h1` and the proof of `¬ x` provided by `h2` to construct a proof of `y`, that can in turn be used to prove our goal, `x ∨ y`, using the introduction rule for `∨` (line 19). To prove `y`, we first construct `H2`: `Prf(¬ y → ⊥)` in a subproof (lines 9-18) and then map it to a proof of `y` using the Lambdapi-axiom encoding double negation elimination, `npp` and the instantiation `¬I(¬y) H2`, that results in type `¬¬y` (line 18). This subproof of `H2`: `Prf(¬y → ⊥)` first assumes `h3`: `Prf(¬y)` and then needs to derive a contradiction in order to provide a term of type `Prf ⊥`. We will do this by constructing a term of type `x = y` based on the two proofs we have for `¬x` (`h2`) and `¬y` (`h3`), which we can then use together with `h1`: `Prf(¬(x = y))` to prove `⊥`. To provide a proof of `x = y`, we once more first show the bidirectional implication, this is done in two subproofs of `H3`: `Prf x → Prf y` (lines 11-13) and `H4`: `Prf y → Prf x` (lines 14-16). Since these subproofs are analogous, we will only discuss the first one. Here, we first assume `h4`: `Prf x` and then provide a proof of `⊥` by showing a contradiction arising from `h4` and `h2`, which proofs `¬x`. This term is given by `¬E x h4 h2`) and, since `⊥E` maps a proof of `⊥` an arbitrary proof-term, we can use it to prove our goal `Prf y`, this is done in line 14. Finally we can then instantiate `propExt` with `x`, `y`, `H3` and `H4` to obtain a term of type `Prf(x = y)` which, along with `h1` of type `Prf(¬(x = y))`, we map to the desired `Prf ⊥` using `¬E` (line 17). As described above, the resulting proof of `¬y → ⊥` is then used to prove `y` (line 18), which in turn is needed for the proof of `x ∨ y`.

The second encoding follows the same pattern:
```
1 opaque symbol NBE_n x y: Prf(¬(x = y)) → Prf(¬ x ∨ ¬ y) :=
2 begin
3   assume x y h1;
4   refine ∨E x (¬ x) (¬ x ∨ ¬ y) ... (em x)
5   {assume h2;
6   have H1: Prf (y) → Prf ⊥
7   {assume h3;
8   have H2: Prf(x) → Prf(y)
9   {assume h4;
10  refine h3};
11   have H3: Prf(y) → Prf(x)
12   {assume h4;
13   refine h2};
14   refine ¬E (x = y) (propExt x y H2 H3) h1};
15   refine ∨Ir (¬ x) (¬ y) (¬I y H1)}
16   {assume h2;
17   refine ∨I1 (¬ x) (¬ y) h2}
18 end;
```

Again, we provide a proof by showing that both `x` and `¬ x` imply `¬ x ∨ ¬ y` and simply proof the latter using of the introduction rule `∨I1` (lines 16 - 17). Here, we however have to prove `Prf(¬ x ∨ ¬ y)` based on the assumption `h1`: `Prf(¬ (x = y))`, which is less complicated, as the proof of `¬ y` we need in place of the proof of `¬ ¬ y` of the previous case is easier to obtain and does not require the elimination of double negation. Furthermore, the proofs of `H2` and `H3` we require to prove `x = y` are more straightforward as we already have assumptions that provide proofs for `x` and `y` themselves rather than their negations (`h2` and `h3` respectively). Otherwise, the proof is analogous.

## D.3 Equal Factoring

The encoding of `(EqFact)` for positive literals is...

```
1 opaque symbol EqFact_p [T] x y z v: ((Prf ((x = y) ∨ (z = v))) → (Prf ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))))) :=
2 begin
3   assume T x y z v h1;
4   refine (∨E (x = y) (¬ (x = y)) ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))) ... )
5   (em (x = y))
6   {assume h2;
7   refine ∨I1 (x = y) ((¬ (x = z)) ∨ (¬ (y = v))) h2}
8   {assume h3;
9   refine (∨E (x = z) (¬ (x = z)) ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))) ... ) (em (x = z))
10  {assume h4;
11  refine (∨E (y = v) (¬ (y = v)) ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))) ... ) (em (y = v))
12   {assume h5;
13   have H1: Prf (z = v)
14   {refine ∨E (x = y) (z = v) (z = v) ... h1
15   {assume h6;
16   refine ⊥E (z = v) (¬E (x = y) h6 h3)}
17   {assume h7;
18   refine h7}};
19   have H2: Prf(x = v)
20   {refine =def [T] x z h4 (λ a, (a = v)) H1};
21   have H3: Prf(v = y)
```
21
22
23
24
25
26
27
28
29

{ refine =def [T] y v h5 (λ a, (v = a)) (=ref [T] v) };
have H4: Prf (x = y)
{ refine =def [T] x v H2 (λ a, (a = y)) H3};
refine ⊥E ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))) (¬E (x = y) H4 h3)}
{assume h8;
refine ∨Ir (x = y) ((¬ (x = z)) ∨ (¬ (y = v))) (∨Ir (¬ (x = z)) (¬ (y = v)) h8)}
{assume h9;
refine ∨Ir (x = y) ((¬ (x = z)) ∨ (¬ (y = v))) (∨I1 (¬ (x = z)) (¬ (y = v)) h9)}
end;

After assuming `T`, `x`, `y`, `z`, `v`, and `h1`: `Prf((x = y) ∨ (z = v))`, we are left with the goal of proving `Prf((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v)))`. To construct this proof, we will perform a series of case distinctions based on the equality relations between `x`, `y`, `z`, and `v`:

We start by instantiating `∀E` as shown in line 4, which results in a term mapping terms of types `Prf (x = y) → Prf (x = y)`, `Prf (¬ (x = y)) → Prf (x = y)` and `Prf ((x = y) ∨ (¬ (x = y)))` to the desired proof-term. The instantiated Lambdapi-axiom of excluded middle (`em (x = y)`) provides the last argument, the first two implications are shown in subproofs. These represent the first case differentiation between `(x = y)` and `¬ (x = y)`. The first subproof is straight forward, as it simply assumes `h2`: `Prf (x = y)` and uses it to prove the goal `Prf ((x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v)))` with `∀I1` (line 6).

For the other subproof, we assume `h3`: `Prf (¬ (x = y))` and proceed to the next case distinction, this time for `x = z` through the analogous application of `∀E` and `em` (line 8). This again results in two subproofs representing the two cases and requiring us to prove `(x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))` based on the assumptions of `h4`: `Prf (x = z)` (line 9) and `h9`: `Prf (¬ (x = z))` (line 27) respectively. The latter is again shown by a nested application of `∀Ir` and `∀I1` to first construct a proof-term of `¬ (x = z) ∨ ¬ (y = v)` based on `h9` and then, based on that, proof `(x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))` (line 28).

For the other subproof, we conduct the last case differentiation, this time for `y = v` (line 10). The subproof for `Prf (¬ (y = v)) → Prf (x = y ∨ (¬ (x = z) ∨ (¬ (y = v)))` is again constructed by assuming `h8`: `Prf (¬ (y = v))` (line 25) and applying nested instances of the introduction rules `∀I1` and `∀Ir` (line 26). The last subproof now uses the assumptions made in the case distinctions to prove `x = y`, which forms a contradiction with `h3`: `Prf (¬ (x = y))` and can hence be used to derive `Prf ⊥`, that in turn can be used to draw an arbitrary conclusion and hence can be applied to the instantiated elimination rule `⊥E` to serve as a proof-term for `(x = y) ∨ (¬ (x = z)) ∨ (¬ (y = v))` (line 24). Proving `x = y` involves several steps: We first construct a term `H1` of type `Prf (z = v)` by showing that it follows from both literals of `h1`: `Prf ((x = y) ∨ (z = v))` and refining with `∀E` (line 13). The subproofs are provided by deriving a contradiction of the assumed `h6`: `Prf (x = y)` and `h3`: `Prf (¬ (x = y))` for the first literal (lines 14 - 15). The second literal corresponds to the assumption of the second subproof (`h7`: `Prf (z = v)`) and is therefore provided as a proof (lines 16 - 17). Furthermore, we proof `H3`: `Prf(v = y)` based on `h5`: `Prf(y = v)` as discussed in Sec. 4.3.2. We now have the following three terms at our disposal: `h4`: `Prf (x = z)`, `H1`: `Prf (z = v)` and `H3`: `Prf(v = y)`. Proving `x = y` thus reduces to the task of proving transitivity of `=` in two instances (lines 18 - 19 and lines 22 - 23). In both cases, this is done with an instantiating of `=def`. This completes the last step of the proof.
Since the proof for the negative version of the rule can be proven analogously, it is not explicitly given here.
E Leo-III TSTP Output for Cantor Subjectivity

thf(sk1_type,type,
sk1: $i > $i > $o ).

thf(sk2_type,type,
sk2: ($i > $o ) > $i ).

thf(1,conjecture,
~ ? [A: $i > $i > $o] :
! [B: $i > $o] :
? [C: $i] :
( ( A @ C )
= B ),
file('sur_cantor.p',sur_cantor) ).

thf(2,negated_conjecture,
~ ~ ? [A: $i > $i > $o] :
! [B: $i > $o] :
? [C: $i] :
( ( A @ C )
= B ),
inference(neg_conjecture,[status(cth)],[1]) ).

thf(3,plain,
~ ~ ? [A: $i > $i > $o] :
! [B: $i > $o] :
? [C: $i] :
( ( A @ C )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(4,plain,
? [A: $i > $i > $o] :
! [B: $i > $o] :
? [C: $i] :
( ( A @ C )
= B ),
inference(polarity_switch,[status(thm)],[3]) ).

thf(5,plain,
! [A: $i > $o] :
( ( sk1 @ ( sk2 @ A ) )
= A ),
inference(cnf,[status(esa)],[4]) ).

thf(6,plain,
! [A: $i > $o] :
( ( sk1 @ ( sk2 @ A ) )
= A ),
inference(lifteq,[status(thm)],[5]) ).

thf(7,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ ( sk2 @ A ) @ B )
= ( A @ B ) ),
inference(func_ext,[status(esa)], [6]) ).

thf(9,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ ( sk2 @ A ) @ B )
| ~ ( A @ B ) ),
inference(bool_ext,[status(thm)], [7]) ).

thf(250,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ ( sk2 @ A ) @ B )
| ( A @ B )
!= ( ~ ( sk1 @ ( sk2 @ A ) @ B ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)], [9]) ).

thf(270,plain,
( sk1
@ ( sk2
@ ^ [A: $i] :
~ ( sk1 @ A @ A ) )
@ ( sk2
@ ^ [A: $i] :
~ ( sk1 @ A @ A ) ) ),
inference(pre_uni,[status(thm)], [250:
[bind(A,$thf( ^ [C: $i] : ~ ( sk1 @ C @ C ) ) ),
bind(B,$thf( sk2 @ ^ [C: $i] : ~ ( sk1 @ C @ C ) ) )]])) ).

thf(8,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1 @ ( sk2 @ A ) @ B )
| ( A @ B ) ),
inference(bool_ext,[status(thm)], [7]) ).

thf(18,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1 @ ( sk2 @ A ) @ B )
| ( A @ B )
!= ( ~ ( sk1 @ ( sk2 @ A ) @ B ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)], [8]) ).

thf(32,plain,
~ ( sk1
@ ( sk2
@ ^ [A: $i] :
~ ( sk1 @ A @ A ) )
@ ( sk2
@ ^ [A: $i] :
~ ( sk1 @ A @ A ) ) ),
inference(pre_uni,[status(thm)], [18:
[bind(A,$thf( ^ [C: $i] : ~ ( sk1 @ C @ C ) ) ),
bind(B,$thf( sk2 @ ^ [C: $i] : ~ ( sk1 @ C @ C ) ) )]]).

thf(372,plain,
$false,
inference(rewrite,[status(thm)],[270,32]) ).

thf(373,plain,
$false,
inference(simp,[status(thm)],[372]) ).
begin
 assume B A;
 have WholeEqFactStep : ((Prf ((sk1 (sk2 A) B) ∨ (¬ (A B)))) → (Prf ((sk1 (sk2 A) B) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ T))))
 {assume h1;
 have TransformToEqLits : (Prf ((¬ ((¬ (sk1 (sk2 A) B)) = T)) ∨ (¬ ((A B) = T))))
 {rewrite .[x in (x ∨ _)] (negEqPosProp_eq (sk1 (sk2 A) B));
 rewrite .[x in (_ ∨ x)] (negEqNegProp_eq (A B));
 refine ((step9 B A));
 have EqFact : (Prf ((¬ ((¬ (sk1 (sk2 A) B)) = T)) ∨ (¬ ((¬ (sk1 (sk2 A) B)) = (A B))) ∨ (¬ (T = T))))
 {refine ((EqFact_n [o] (¬ (sk1 (sk2 A) B)) T (A B) T) TransformToEqLits)};
 have EqSymmetry : (Prf ((¬ ((¬ (sk1 (sk2 A) B)) = T)) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ (T = T))))
 {rewrite .[x in (_ ∨ ¬ x ∨ _)] (eqSym_eq [o]);
 refine (EqFact)};
 have TransformToNonEqLits : (Prf ((sk1 (sk2 A) B) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ T)))
 {rewrite .[x in (x ∨ _ ∨ _)] posPropNegEq_eq;
 rewrite .[x in (_ ∨ _ ∨ x)] negPropNegEq_eq;
 refine (EqSymmetry)};
 refine (TransformToNonEqLits);
 refine (WholeEqFactStep (step9 B A))
end;

// PreUni
opaque symbol step265: ((Prf ((sk1 (sk2 (λ (A : (El ι)), (¬ (sk1 A A)))) (sk2 (λ (A : (El ι)), (¬ (sk1 A A)))))) :=
begin
 have Substitution : (Prf ((sk1 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) ∨ (¬ (((λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) = (¬ (sk1 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))) ∨ (¬ T))))
 {refine (step252 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (λ (C : (El ι)), (¬ (sk1 C C))));
 rewrite simp7_eq;
 rewrite .[x in (_ ∨ x)] (simp10_eq o ((λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))
 rewrite .[x in (_ ∨ x)] simp7_eq;
 rewrite .[x in (_ ∨ _ ∨ x)] simp16_eq;
 refine (Substitution)
end;

// BoolExt
opaque symbol step8: (Π (B : (El ι)), Π (A : (El (ι ↦ o))), (Prf ((¬ (sk1 (sk2 A B)) ∨ (A B)))) :=
begin
 assume B A;
 refine ((PBE_1 (sk1 (sk2 A) B) (A B)) (step7 B A))
end;

// OrderedEqFac
opaque symbol step18: (Π (B : (El ι)), Π (A : (El (ι ↦ o))), (Prf ((¬ (sk1 (sk2 A B)) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ T)))) :=
begin
 assume B A;
```pascal
have WholeEqFactStep : ((Prf ((¬ (sk1 (sk2 A) B)) ∨ (A B))) → (Prf ((¬ (sk1 (sk2 A) B)) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ T)))))
{assume h1;
have TransformToEqLits : (Prf (((¬ (sk1 (sk2 A) B)) = T) ∨ ((A B) = T)))
{rewrite .[x in (x ∨ _)] posEqNegProp_eq;
rewrite .[x in (_ ∨ x)] (posEqPosProp_eq (A B));
refine ((step8 B A))};
have EqFact : (Prf (((¬ (sk1 (sk2 A) B)) = T) ∨ (¬ ((¬ (sk1 (sk2 A) B)) = (A B))) ∨ (¬ (T = T)))))
{refine ((EqFact_p [o] (¬ (sk1 (sk2 A) B)) T (A B) T) TransformToEqLits)};
have EqSymmetry : (Prf (((¬ (sk1 (sk2 A) B)) = T) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ (T = T)))))
{rewrite .[x in (_ ∨ ¬ x ∨ _)] (eqSym_eq [o]);
refine (EqFact)};
have TransformToNonEqLits : (Prf ((¬ (sk1 (sk2 A) B)) ∨ (¬ ((A B) = (¬ (sk1 (sk2 A) B)))) ∨ (¬ T)))
{rewrite .[x in (x ∨ _ ∨ _)] negPropPosEq_eq;
rewrite .[x in (_ ∨ _ ∨ x)] negPropNegEq_eq;
refine (EqSymmetry)};
refine (TransformToNonEqLits)};
refine (WholeEqFactStep (step8 B A))
end;

// PreUni
opaque symbol step33: ((Prf ((¬ (sk1 (sk2 (λ (A : (El ι)), (¬ (sk1 A A)))) (sk2 (λ (A : (El ι)), (¬ (sk1 A A)))))) :=
begin
have Substitution : (Prf ((¬ (sk1 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))) ∨ (¬ (((λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))) = (¬ (sk1 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))) ∨ (¬ T))))
{refine (step18 (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))) (λ (C : (El ι)), (¬ (sk1 C C))));
rewrite simp7_eq;
rewrite .[x in (_ ∨ x)] (simp10_eq o ((λ (C : (El ι)), (¬ (sk1 C C)))) (sk2 (λ (C : (El ι)), (¬ (sk1 C C)))))
rewrite .[x in (_ ∨ x)] simp7_eq;
rewrite .[x in (_ ∨ _ ∨ x)] simp16_eq;
refine (Substitution)
end;

// RewriteSimp
opaque symbol step373: ((Prf (⊥))) :=
begin
have TransformToEqLits : (Prf (⊥ = (sk1 (sk2 (λ (A : (El ι)), (¬ (sk1 A A)))) (sk2 (λ (A : (El ι)), (¬ (sk1 A A))))))
{rewrite botNegProp_eq;
refine (step33)};
rewrite TransformToEqLits;
refine (step265)
end;
```