harp-project / AML-Formalization

GNU Lesser General Public License v2.1
10 stars 5 forks source link

Sum sort theory #430

Closed adilido99 closed 6 months ago

adilido99 commented 6 months ago

the following theorems need to be named and moved: t1, t2, unnamed, unnamed_1 the admits are as follows: t3, membership_axiom_v1/v2

adilido99 commented 6 months ago

changes resolved, ready to merge :)

adilido99 commented 6 months ago

changes made