Skip to main content

oxilean_std/set/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7#[allow(dead_code)]
8pub fn app(f: Expr, a: Expr) -> Expr {
9    Expr::App(Box::new(f), Box::new(a))
10}
11#[allow(dead_code)]
12pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
13    app(app(f, a), b)
14}
15#[allow(dead_code)]
16pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
17    app(app2(f, a, b), c)
18}
19#[allow(dead_code)]
20pub fn app4(f: Expr, a: Expr, b: Expr, c: Expr, d: Expr) -> Expr {
21    app(app3(f, a, b, c), d)
22}
23pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
24    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
25}
26#[allow(dead_code)]
27pub fn lam(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
28    Expr::Lam(bi, Name::str(name), Box::new(dom), Box::new(body))
29}
30pub(super) fn cst(s: &str) -> Expr {
31    Expr::Const(Name::str(s), vec![])
32}
33#[allow(dead_code)]
34pub fn cst_u(s: &str, levels: Vec<Level>) -> Expr {
35    Expr::Const(Name::str(s), levels)
36}
37pub fn prop() -> Expr {
38    Expr::Sort(Level::zero())
39}
40pub fn type0() -> Expr {
41    Expr::Sort(Level::succ(Level::zero()))
42}
43#[allow(dead_code)]
44pub fn type1() -> Expr {
45    Expr::Sort(Level::succ(Level::succ(Level::zero())))
46}
47#[allow(dead_code)]
48pub fn sort_u() -> Expr {
49    Expr::Sort(Level::Param(Name::str("u")))
50}
51#[allow(dead_code)]
52pub fn sort_v() -> Expr {
53    Expr::Sort(Level::Param(Name::str("v")))
54}
55pub fn bvar(n: u32) -> Expr {
56    Expr::BVar(n)
57}
58pub fn arrow(a: Expr, b: Expr) -> Expr {
59    Expr::Pi(
60        BinderInfo::Default,
61        Name::Anonymous,
62        Box::new(a),
63        Box::new(b),
64    )
65}
66pub(super) fn nat_ty() -> Expr {
67    Expr::Const(Name::str("Nat"), vec![])
68}
69pub fn add_axiom(
70    env: &mut Environment,
71    name: &str,
72    univ_params: Vec<Name>,
73    ty: Expr,
74) -> Result<(), String> {
75    env.add(Declaration::Axiom {
76        name: Name::str(name),
77        univ_params,
78        ty,
79    })
80    .map_err(|e| e.to_string())
81}
82/// Build `Set α` — which is `α → Prop`.
83/// `elem_ty` is the expression for `α`.
84#[allow(dead_code)]
85pub(super) fn set_ty_of(elem_ty: Expr) -> Expr {
86    arrow(elem_ty, prop())
87}
88/// Build `Eq @{} T a b`.
89#[allow(dead_code)]
90pub(super) fn mk_eq_expr(ty: Expr, lhs: Expr, rhs: Expr) -> Expr {
91    app3(cst("Eq"), ty, lhs, rhs)
92}
93/// Build the set theory environment containing set types, operations, and theorems.
94#[allow(clippy::too_many_lines)]
95pub fn build_set_env(env: &mut Environment) -> Result<(), String> {
96    add_axiom(env, "Set", vec![], arrow(type0(), type0()))?;
97    let set_mem_ty = pi(
98        BinderInfo::Implicit,
99        "α",
100        type0(),
101        pi(
102            BinderInfo::Default,
103            "a",
104            bvar(0),
105            pi(BinderInfo::Default, "s", app(cst("Set"), bvar(1)), prop()),
106        ),
107    );
108    add_axiom(env, "Set.mem", vec![], set_mem_ty)?;
109    let set_empty_ty = pi(BinderInfo::Implicit, "α", type0(), app(cst("Set"), bvar(0)));
110    add_axiom(env, "Set.empty", vec![], set_empty_ty)?;
111    let set_univ_ty = pi(BinderInfo::Implicit, "α", type0(), app(cst("Set"), bvar(0)));
112    add_axiom(env, "Set.univ", vec![], set_univ_ty)?;
113    let set_singleton_ty = pi(
114        BinderInfo::Implicit,
115        "α",
116        type0(),
117        pi(BinderInfo::Default, "a", bvar(0), app(cst("Set"), bvar(1))),
118    );
119    add_axiom(env, "Set.singleton", vec![], set_singleton_ty)?;
120    let set_union_ty = pi(
121        BinderInfo::Implicit,
122        "α",
123        type0(),
124        pi(
125            BinderInfo::Default,
126            "s",
127            app(cst("Set"), bvar(0)),
128            pi(
129                BinderInfo::Default,
130                "t",
131                app(cst("Set"), bvar(1)),
132                app(cst("Set"), bvar(2)),
133            ),
134        ),
135    );
136    add_axiom(env, "Set.union", vec![], set_union_ty)?;
137    let set_inter_ty = pi(
138        BinderInfo::Implicit,
139        "α",
140        type0(),
141        pi(
142            BinderInfo::Default,
143            "s",
144            app(cst("Set"), bvar(0)),
145            pi(
146                BinderInfo::Default,
147                "t",
148                app(cst("Set"), bvar(1)),
149                app(cst("Set"), bvar(2)),
150            ),
151        ),
152    );
153    add_axiom(env, "Set.inter", vec![], set_inter_ty)?;
154    let set_diff_ty = pi(
155        BinderInfo::Implicit,
156        "α",
157        type0(),
158        pi(
159            BinderInfo::Default,
160            "s",
161            app(cst("Set"), bvar(0)),
162            pi(
163                BinderInfo::Default,
164                "t",
165                app(cst("Set"), bvar(1)),
166                app(cst("Set"), bvar(2)),
167            ),
168        ),
169    );
170    add_axiom(env, "Set.diff", vec![], set_diff_ty)?;
171    let set_compl_ty = pi(
172        BinderInfo::Implicit,
173        "α",
174        type0(),
175        pi(
176            BinderInfo::Default,
177            "s",
178            app(cst("Set"), bvar(0)),
179            app(cst("Set"), bvar(1)),
180        ),
181    );
182    add_axiom(env, "Set.compl", vec![], set_compl_ty)?;
183    let set_subset_ty = pi(
184        BinderInfo::Implicit,
185        "α",
186        type0(),
187        pi(
188            BinderInfo::Default,
189            "s",
190            app(cst("Set"), bvar(0)),
191            pi(BinderInfo::Default, "t", app(cst("Set"), bvar(1)), prop()),
192        ),
193    );
194    add_axiom(env, "Set.subset", vec![], set_subset_ty)?;
195    let set_ssubset_ty = pi(
196        BinderInfo::Implicit,
197        "α",
198        type0(),
199        pi(
200            BinderInfo::Default,
201            "s",
202            app(cst("Set"), bvar(0)),
203            pi(BinderInfo::Default, "t", app(cst("Set"), bvar(1)), prop()),
204        ),
205    );
206    add_axiom(env, "Set.ssubset", vec![], set_ssubset_ty)?;
207    let set_image_ty = pi(
208        BinderInfo::Implicit,
209        "α",
210        type0(),
211        pi(
212            BinderInfo::Implicit,
213            "β",
214            type0(),
215            pi(
216                BinderInfo::Default,
217                "f",
218                arrow(bvar(1), bvar(1)),
219                pi(
220                    BinderInfo::Default,
221                    "s",
222                    app(cst("Set"), bvar(2)),
223                    app(cst("Set"), bvar(2)),
224                ),
225            ),
226        ),
227    );
228    add_axiom(env, "Set.image", vec![], set_image_ty)?;
229    let set_preimage_ty = pi(
230        BinderInfo::Implicit,
231        "α",
232        type0(),
233        pi(
234            BinderInfo::Implicit,
235            "β",
236            type0(),
237            pi(
238                BinderInfo::Default,
239                "f",
240                arrow(bvar(1), bvar(1)),
241                pi(
242                    BinderInfo::Default,
243                    "s",
244                    app(cst("Set"), bvar(1)),
245                    app(cst("Set"), bvar(3)),
246                ),
247            ),
248        ),
249    );
250    add_axiom(env, "Set.preimage", vec![], set_preimage_ty)?;
251    let set_range_ty = pi(
252        BinderInfo::Implicit,
253        "α",
254        type0(),
255        pi(
256            BinderInfo::Implicit,
257            "β",
258            type0(),
259            pi(
260                BinderInfo::Default,
261                "f",
262                arrow(bvar(1), bvar(1)),
263                app(cst("Set"), bvar(1)),
264            ),
265        ),
266    );
267    add_axiom(env, "Set.range", vec![], set_range_ty)?;
268    let set_sep_ty = pi(
269        BinderInfo::Implicit,
270        "α",
271        type0(),
272        pi(
273            BinderInfo::Default,
274            "s",
275            app(cst("Set"), bvar(0)),
276            pi(
277                BinderInfo::Default,
278                "p",
279                arrow(bvar(1), prop()),
280                app(cst("Set"), bvar(2)),
281            ),
282        ),
283    );
284    add_axiom(env, "Set.sep", vec![], set_sep_ty)?;
285    let set_insert_ty = pi(
286        BinderInfo::Implicit,
287        "α",
288        type0(),
289        pi(
290            BinderInfo::Default,
291            "a",
292            bvar(0),
293            pi(
294                BinderInfo::Default,
295                "s",
296                app(cst("Set"), bvar(1)),
297                app(cst("Set"), bvar(2)),
298            ),
299        ),
300    );
301    add_axiom(env, "Set.insert", vec![], set_insert_ty)?;
302    let set_erase_ty = pi(
303        BinderInfo::Implicit,
304        "α",
305        type0(),
306        pi(
307            BinderInfo::InstImplicit,
308            "_inst",
309            app(cst("DecidableEq"), bvar(0)),
310            pi(
311                BinderInfo::Default,
312                "s",
313                app(cst("Set"), bvar(1)),
314                pi(BinderInfo::Default, "a", bvar(2), app(cst("Set"), bvar(3))),
315            ),
316        ),
317    );
318    add_axiom(env, "Set.erase", vec![], set_erase_ty)?;
319    let mem_union_ty = pi(
320        BinderInfo::Implicit,
321        "α",
322        type0(),
323        pi(
324            BinderInfo::Implicit,
325            "a",
326            bvar(0),
327            pi(
328                BinderInfo::Implicit,
329                "s",
330                app(cst("Set"), bvar(1)),
331                pi(
332                    BinderInfo::Implicit,
333                    "t",
334                    app(cst("Set"), bvar(2)),
335                    app2(
336                        cst("Iff"),
337                        app2(
338                            cst("Set.mem"),
339                            bvar(2),
340                            app2(cst("Set.union"), bvar(1), bvar(0)),
341                        ),
342                        app2(
343                            cst("Or"),
344                            app2(cst("Set.mem"), bvar(2), bvar(1)),
345                            app2(cst("Set.mem"), bvar(2), bvar(0)),
346                        ),
347                    ),
348                ),
349            ),
350        ),
351    );
352    add_axiom(env, "Set.mem_union", vec![], mem_union_ty)?;
353    let mem_inter_ty = pi(
354        BinderInfo::Implicit,
355        "α",
356        type0(),
357        pi(
358            BinderInfo::Implicit,
359            "a",
360            bvar(0),
361            pi(
362                BinderInfo::Implicit,
363                "s",
364                app(cst("Set"), bvar(1)),
365                pi(
366                    BinderInfo::Implicit,
367                    "t",
368                    app(cst("Set"), bvar(2)),
369                    app2(
370                        cst("Iff"),
371                        app2(
372                            cst("Set.mem"),
373                            bvar(2),
374                            app2(cst("Set.inter"), bvar(1), bvar(0)),
375                        ),
376                        app2(
377                            cst("And"),
378                            app2(cst("Set.mem"), bvar(2), bvar(1)),
379                            app2(cst("Set.mem"), bvar(2), bvar(0)),
380                        ),
381                    ),
382                ),
383            ),
384        ),
385    );
386    add_axiom(env, "Set.mem_inter", vec![], mem_inter_ty)?;
387    let mem_diff_ty = pi(
388        BinderInfo::Implicit,
389        "α",
390        type0(),
391        pi(
392            BinderInfo::Implicit,
393            "a",
394            bvar(0),
395            pi(
396                BinderInfo::Implicit,
397                "s",
398                app(cst("Set"), bvar(1)),
399                pi(
400                    BinderInfo::Implicit,
401                    "t",
402                    app(cst("Set"), bvar(2)),
403                    app2(
404                        cst("Iff"),
405                        app2(
406                            cst("Set.mem"),
407                            bvar(2),
408                            app2(cst("Set.diff"), bvar(1), bvar(0)),
409                        ),
410                        app2(
411                            cst("And"),
412                            app2(cst("Set.mem"), bvar(2), bvar(1)),
413                            app(cst("Not"), app2(cst("Set.mem"), bvar(2), bvar(0))),
414                        ),
415                    ),
416                ),
417            ),
418        ),
419    );
420    add_axiom(env, "Set.mem_diff", vec![], mem_diff_ty)?;
421    let mem_compl_ty = pi(
422        BinderInfo::Implicit,
423        "α",
424        type0(),
425        pi(
426            BinderInfo::Implicit,
427            "a",
428            bvar(0),
429            pi(
430                BinderInfo::Implicit,
431                "s",
432                app(cst("Set"), bvar(1)),
433                app2(
434                    cst("Iff"),
435                    app2(cst("Set.mem"), bvar(1), app(cst("Set.compl"), bvar(0))),
436                    app(cst("Not"), app2(cst("Set.mem"), bvar(1), bvar(0))),
437                ),
438            ),
439        ),
440    );
441    add_axiom(env, "Set.mem_compl", vec![], mem_compl_ty)?;
442    let union_comm_ty = pi(
443        BinderInfo::Implicit,
444        "α",
445        type0(),
446        pi(
447            BinderInfo::Default,
448            "s",
449            app(cst("Set"), bvar(0)),
450            pi(
451                BinderInfo::Default,
452                "t",
453                app(cst("Set"), bvar(1)),
454                mk_eq_expr(
455                    app(cst("Set"), bvar(2)),
456                    app2(cst("Set.union"), bvar(1), bvar(0)),
457                    app2(cst("Set.union"), bvar(0), bvar(1)),
458                ),
459            ),
460        ),
461    );
462    add_axiom(env, "Set.union_comm", vec![], union_comm_ty)?;
463    let union_assoc_ty = pi(
464        BinderInfo::Implicit,
465        "α",
466        type0(),
467        pi(
468            BinderInfo::Default,
469            "s",
470            app(cst("Set"), bvar(0)),
471            pi(
472                BinderInfo::Default,
473                "t",
474                app(cst("Set"), bvar(1)),
475                pi(
476                    BinderInfo::Default,
477                    "u",
478                    app(cst("Set"), bvar(2)),
479                    mk_eq_expr(
480                        app(cst("Set"), bvar(3)),
481                        app2(
482                            cst("Set.union"),
483                            app2(cst("Set.union"), bvar(2), bvar(1)),
484                            bvar(0),
485                        ),
486                        app2(
487                            cst("Set.union"),
488                            bvar(2),
489                            app2(cst("Set.union"), bvar(1), bvar(0)),
490                        ),
491                    ),
492                ),
493            ),
494        ),
495    );
496    add_axiom(env, "Set.union_assoc", vec![], union_assoc_ty)?;
497    let inter_comm_ty = pi(
498        BinderInfo::Implicit,
499        "α",
500        type0(),
501        pi(
502            BinderInfo::Default,
503            "s",
504            app(cst("Set"), bvar(0)),
505            pi(
506                BinderInfo::Default,
507                "t",
508                app(cst("Set"), bvar(1)),
509                mk_eq_expr(
510                    app(cst("Set"), bvar(2)),
511                    app2(cst("Set.inter"), bvar(1), bvar(0)),
512                    app2(cst("Set.inter"), bvar(0), bvar(1)),
513                ),
514            ),
515        ),
516    );
517    add_axiom(env, "Set.inter_comm", vec![], inter_comm_ty)?;
518    let inter_assoc_ty = pi(
519        BinderInfo::Implicit,
520        "α",
521        type0(),
522        pi(
523            BinderInfo::Default,
524            "s",
525            app(cst("Set"), bvar(0)),
526            pi(
527                BinderInfo::Default,
528                "t",
529                app(cst("Set"), bvar(1)),
530                pi(
531                    BinderInfo::Default,
532                    "u",
533                    app(cst("Set"), bvar(2)),
534                    mk_eq_expr(
535                        app(cst("Set"), bvar(3)),
536                        app2(
537                            cst("Set.inter"),
538                            app2(cst("Set.inter"), bvar(2), bvar(1)),
539                            bvar(0),
540                        ),
541                        app2(
542                            cst("Set.inter"),
543                            bvar(2),
544                            app2(cst("Set.inter"), bvar(1), bvar(0)),
545                        ),
546                    ),
547                ),
548            ),
549        ),
550    );
551    add_axiom(env, "Set.inter_assoc", vec![], inter_assoc_ty)?;
552    let union_empty_ty = pi(
553        BinderInfo::Implicit,
554        "α",
555        type0(),
556        pi(
557            BinderInfo::Default,
558            "s",
559            app(cst("Set"), bvar(0)),
560            mk_eq_expr(
561                app(cst("Set"), bvar(1)),
562                app2(cst("Set.union"), bvar(0), cst("Set.empty")),
563                bvar(0),
564            ),
565        ),
566    );
567    add_axiom(env, "Set.union_empty", vec![], union_empty_ty)?;
568    let empty_union_ty = pi(
569        BinderInfo::Implicit,
570        "α",
571        type0(),
572        pi(
573            BinderInfo::Default,
574            "s",
575            app(cst("Set"), bvar(0)),
576            mk_eq_expr(
577                app(cst("Set"), bvar(1)),
578                app2(cst("Set.union"), cst("Set.empty"), bvar(0)),
579                bvar(0),
580            ),
581        ),
582    );
583    add_axiom(env, "Set.empty_union", vec![], empty_union_ty)?;
584    let inter_univ_ty = pi(
585        BinderInfo::Implicit,
586        "α",
587        type0(),
588        pi(
589            BinderInfo::Default,
590            "s",
591            app(cst("Set"), bvar(0)),
592            mk_eq_expr(
593                app(cst("Set"), bvar(1)),
594                app2(cst("Set.inter"), bvar(0), cst("Set.univ")),
595                bvar(0),
596            ),
597        ),
598    );
599    add_axiom(env, "Set.inter_univ", vec![], inter_univ_ty)?;
600    let univ_inter_ty = pi(
601        BinderInfo::Implicit,
602        "α",
603        type0(),
604        pi(
605            BinderInfo::Default,
606            "s",
607            app(cst("Set"), bvar(0)),
608            mk_eq_expr(
609                app(cst("Set"), bvar(1)),
610                app2(cst("Set.inter"), cst("Set.univ"), bvar(0)),
611                bvar(0),
612            ),
613        ),
614    );
615    add_axiom(env, "Set.univ_inter", vec![], univ_inter_ty)?;
616    let subset_refl_ty = pi(
617        BinderInfo::Implicit,
618        "α",
619        type0(),
620        pi(
621            BinderInfo::Default,
622            "s",
623            app(cst("Set"), bvar(0)),
624            app2(cst("Set.subset"), bvar(0), bvar(0)),
625        ),
626    );
627    add_axiom(env, "Set.subset_refl", vec![], subset_refl_ty)?;
628    let subset_trans_ty = pi(
629        BinderInfo::Implicit,
630        "α",
631        type0(),
632        pi(
633            BinderInfo::Implicit,
634            "s",
635            app(cst("Set"), bvar(0)),
636            pi(
637                BinderInfo::Implicit,
638                "t",
639                app(cst("Set"), bvar(1)),
640                pi(
641                    BinderInfo::Implicit,
642                    "u",
643                    app(cst("Set"), bvar(2)),
644                    pi(
645                        BinderInfo::Default,
646                        "h1",
647                        app2(cst("Set.subset"), bvar(2), bvar(1)),
648                        pi(
649                            BinderInfo::Default,
650                            "h2",
651                            app2(cst("Set.subset"), bvar(2), bvar(1)),
652                            app2(cst("Set.subset"), bvar(4), bvar(2)),
653                        ),
654                    ),
655                ),
656            ),
657        ),
658    );
659    add_axiom(env, "Set.subset_trans", vec![], subset_trans_ty)?;
660    let subset_antisymm_ty = pi(
661        BinderInfo::Implicit,
662        "α",
663        type0(),
664        pi(
665            BinderInfo::Implicit,
666            "s",
667            app(cst("Set"), bvar(0)),
668            pi(
669                BinderInfo::Implicit,
670                "t",
671                app(cst("Set"), bvar(1)),
672                pi(
673                    BinderInfo::Default,
674                    "h1",
675                    app2(cst("Set.subset"), bvar(1), bvar(0)),
676                    pi(
677                        BinderInfo::Default,
678                        "h2",
679                        app2(cst("Set.subset"), bvar(1), bvar(2)),
680                        mk_eq_expr(app(cst("Set"), bvar(4)), bvar(3), bvar(2)),
681                    ),
682                ),
683            ),
684        ),
685    );
686    add_axiom(env, "Set.subset_antisymm", vec![], subset_antisymm_ty)?;
687    let uid_ty = pi(
688        BinderInfo::Implicit,
689        "α",
690        type0(),
691        pi(
692            BinderInfo::Default,
693            "s",
694            app(cst("Set"), bvar(0)),
695            pi(
696                BinderInfo::Default,
697                "t",
698                app(cst("Set"), bvar(1)),
699                pi(
700                    BinderInfo::Default,
701                    "u",
702                    app(cst("Set"), bvar(2)),
703                    mk_eq_expr(
704                        app(cst("Set"), bvar(3)),
705                        app2(
706                            cst("Set.union"),
707                            bvar(2),
708                            app2(cst("Set.inter"), bvar(1), bvar(0)),
709                        ),
710                        app2(
711                            cst("Set.inter"),
712                            app2(cst("Set.union"), bvar(2), bvar(1)),
713                            app2(cst("Set.union"), bvar(2), bvar(0)),
714                        ),
715                    ),
716                ),
717            ),
718        ),
719    );
720    add_axiom(env, "Set.union_inter_distrib", vec![], uid_ty)?;
721    let iud_ty = pi(
722        BinderInfo::Implicit,
723        "α",
724        type0(),
725        pi(
726            BinderInfo::Default,
727            "s",
728            app(cst("Set"), bvar(0)),
729            pi(
730                BinderInfo::Default,
731                "t",
732                app(cst("Set"), bvar(1)),
733                pi(
734                    BinderInfo::Default,
735                    "u",
736                    app(cst("Set"), bvar(2)),
737                    mk_eq_expr(
738                        app(cst("Set"), bvar(3)),
739                        app2(
740                            cst("Set.inter"),
741                            bvar(2),
742                            app2(cst("Set.union"), bvar(1), bvar(0)),
743                        ),
744                        app2(
745                            cst("Set.union"),
746                            app2(cst("Set.inter"), bvar(2), bvar(1)),
747                            app2(cst("Set.inter"), bvar(2), bvar(0)),
748                        ),
749                    ),
750                ),
751            ),
752        ),
753    );
754    add_axiom(env, "Set.inter_union_distrib", vec![], iud_ty)?;
755    let compl_compl_ty = pi(
756        BinderInfo::Implicit,
757        "α",
758        type0(),
759        pi(
760            BinderInfo::Default,
761            "s",
762            app(cst("Set"), bvar(0)),
763            mk_eq_expr(
764                app(cst("Set"), bvar(1)),
765                app(cst("Set.compl"), app(cst("Set.compl"), bvar(0))),
766                bvar(0),
767            ),
768        ),
769    );
770    add_axiom(env, "Set.compl_compl", vec![], compl_compl_ty)?;
771    let compl_union_ty = pi(
772        BinderInfo::Implicit,
773        "α",
774        type0(),
775        pi(
776            BinderInfo::Default,
777            "s",
778            app(cst("Set"), bvar(0)),
779            pi(
780                BinderInfo::Default,
781                "t",
782                app(cst("Set"), bvar(1)),
783                mk_eq_expr(
784                    app(cst("Set"), bvar(2)),
785                    app(cst("Set.compl"), app2(cst("Set.union"), bvar(1), bvar(0))),
786                    app2(
787                        cst("Set.inter"),
788                        app(cst("Set.compl"), bvar(1)),
789                        app(cst("Set.compl"), bvar(0)),
790                    ),
791                ),
792            ),
793        ),
794    );
795    add_axiom(env, "Set.compl_union", vec![], compl_union_ty)?;
796    let compl_inter_ty = pi(
797        BinderInfo::Implicit,
798        "α",
799        type0(),
800        pi(
801            BinderInfo::Default,
802            "s",
803            app(cst("Set"), bvar(0)),
804            pi(
805                BinderInfo::Default,
806                "t",
807                app(cst("Set"), bvar(1)),
808                mk_eq_expr(
809                    app(cst("Set"), bvar(2)),
810                    app(cst("Set.compl"), app2(cst("Set.inter"), bvar(1), bvar(0))),
811                    app2(
812                        cst("Set.union"),
813                        app(cst("Set.compl"), bvar(1)),
814                        app(cst("Set.compl"), bvar(0)),
815                    ),
816                ),
817            ),
818        ),
819    );
820    add_axiom(env, "Set.compl_inter", vec![], compl_inter_ty)?;
821    let image_comp_ty = pi(
822        BinderInfo::Implicit,
823        "α",
824        type0(),
825        pi(
826            BinderInfo::Implicit,
827            "β",
828            type0(),
829            pi(
830                BinderInfo::Implicit,
831                "γ",
832                type0(),
833                pi(
834                    BinderInfo::Default,
835                    "g",
836                    arrow(bvar(1), bvar(1)),
837                    pi(
838                        BinderInfo::Default,
839                        "f",
840                        arrow(bvar(3), bvar(3)),
841                        pi(
842                            BinderInfo::Default,
843                            "s",
844                            app(cst("Set"), bvar(4)),
845                            mk_eq_expr(
846                                app(cst("Set"), bvar(3)),
847                                app2(
848                                    cst("Set.image"),
849                                    bvar(2),
850                                    app2(cst("Set.image"), bvar(1), bvar(0)),
851                                ),
852                                app2(
853                                    cst("Set.image"),
854                                    lam(
855                                        BinderInfo::Default,
856                                        "x",
857                                        bvar(5),
858                                        app(bvar(3), app(bvar(2), bvar(0))),
859                                    ),
860                                    bvar(0),
861                                ),
862                            ),
863                        ),
864                    ),
865                ),
866            ),
867        ),
868    );
869    add_axiom(env, "Set.image_comp", vec![], image_comp_ty)?;
870    let preimage_comp_ty = pi(
871        BinderInfo::Implicit,
872        "α",
873        type0(),
874        pi(
875            BinderInfo::Implicit,
876            "β",
877            type0(),
878            pi(
879                BinderInfo::Implicit,
880                "γ",
881                type0(),
882                pi(
883                    BinderInfo::Default,
884                    "g",
885                    arrow(bvar(1), bvar(1)),
886                    pi(
887                        BinderInfo::Default,
888                        "f",
889                        arrow(bvar(3), bvar(3)),
890                        pi(
891                            BinderInfo::Default,
892                            "s",
893                            app(cst("Set"), bvar(2)),
894                            mk_eq_expr(
895                                app(cst("Set"), bvar(5)),
896                                app2(
897                                    cst("Set.preimage"),
898                                    bvar(1),
899                                    app2(cst("Set.preimage"), bvar(2), bvar(0)),
900                                ),
901                                app2(
902                                    cst("Set.preimage"),
903                                    lam(
904                                        BinderInfo::Default,
905                                        "x",
906                                        bvar(5),
907                                        app(bvar(3), app(bvar(2), bvar(0))),
908                                    ),
909                                    bvar(0),
910                                ),
911                            ),
912                        ),
913                    ),
914                ),
915            ),
916        ),
917    );
918    add_axiom(env, "Set.preimage_comp", vec![], preimage_comp_ty)?;
919    let image_union_ty = pi(
920        BinderInfo::Implicit,
921        "α",
922        type0(),
923        pi(
924            BinderInfo::Implicit,
925            "β",
926            type0(),
927            pi(
928                BinderInfo::Default,
929                "f",
930                arrow(bvar(1), bvar(1)),
931                pi(
932                    BinderInfo::Default,
933                    "s",
934                    app(cst("Set"), bvar(2)),
935                    pi(
936                        BinderInfo::Default,
937                        "t",
938                        app(cst("Set"), bvar(3)),
939                        mk_eq_expr(
940                            app(cst("Set"), bvar(3)),
941                            app2(
942                                cst("Set.image"),
943                                bvar(2),
944                                app2(cst("Set.union"), bvar(1), bvar(0)),
945                            ),
946                            app2(
947                                cst("Set.union"),
948                                app2(cst("Set.image"), bvar(2), bvar(1)),
949                                app2(cst("Set.image"), bvar(2), bvar(0)),
950                            ),
951                        ),
952                    ),
953                ),
954            ),
955        ),
956    );
957    add_axiom(env, "Set.image_union", vec![], image_union_ty)?;
958    let image_inter_subset_ty = pi(
959        BinderInfo::Implicit,
960        "α",
961        type0(),
962        pi(
963            BinderInfo::Implicit,
964            "β",
965            type0(),
966            pi(
967                BinderInfo::Default,
968                "f",
969                arrow(bvar(1), bvar(1)),
970                pi(
971                    BinderInfo::Default,
972                    "s",
973                    app(cst("Set"), bvar(2)),
974                    pi(
975                        BinderInfo::Default,
976                        "t",
977                        app(cst("Set"), bvar(3)),
978                        app2(
979                            cst("Set.subset"),
980                            app2(
981                                cst("Set.image"),
982                                bvar(2),
983                                app2(cst("Set.inter"), bvar(1), bvar(0)),
984                            ),
985                            app2(
986                                cst("Set.inter"),
987                                app2(cst("Set.image"), bvar(2), bvar(1)),
988                                app2(cst("Set.image"), bvar(2), bvar(0)),
989                            ),
990                        ),
991                    ),
992                ),
993            ),
994        ),
995    );
996    add_axiom(env, "Set.image_inter_subset", vec![], image_inter_subset_ty)?;
997    add_axiom(env, "Finset", vec![], arrow(type0(), type0()))?;
998    let finset_empty_ty = pi(
999        BinderInfo::Implicit,
1000        "α",
1001        type0(),
1002        app(cst("Finset"), bvar(0)),
1003    );
1004    add_axiom(env, "Finset.empty", vec![], finset_empty_ty)?;
1005    let finset_insert_ty = pi(
1006        BinderInfo::Implicit,
1007        "α",
1008        type0(),
1009        pi(
1010            BinderInfo::InstImplicit,
1011            "_inst",
1012            app(cst("DecidableEq"), bvar(0)),
1013            pi(
1014                BinderInfo::Default,
1015                "a",
1016                bvar(1),
1017                pi(
1018                    BinderInfo::Default,
1019                    "s",
1020                    app(cst("Finset"), bvar(2)),
1021                    app(cst("Finset"), bvar(3)),
1022                ),
1023            ),
1024        ),
1025    );
1026    add_axiom(env, "Finset.insert", vec![], finset_insert_ty)?;
1027    let finset_card_ty = pi(
1028        BinderInfo::Implicit,
1029        "α",
1030        type0(),
1031        pi(
1032            BinderInfo::Default,
1033            "s",
1034            app(cst("Finset"), bvar(0)),
1035            nat_ty(),
1036        ),
1037    );
1038    add_axiom(env, "Finset.card", vec![], finset_card_ty)?;
1039    let finset_union_ty = pi(
1040        BinderInfo::Implicit,
1041        "α",
1042        type0(),
1043        pi(
1044            BinderInfo::InstImplicit,
1045            "_inst",
1046            app(cst("DecidableEq"), bvar(0)),
1047            pi(
1048                BinderInfo::Default,
1049                "s",
1050                app(cst("Finset"), bvar(1)),
1051                pi(
1052                    BinderInfo::Default,
1053                    "t",
1054                    app(cst("Finset"), bvar(2)),
1055                    app(cst("Finset"), bvar(3)),
1056                ),
1057            ),
1058        ),
1059    );
1060    add_axiom(env, "Finset.union", vec![], finset_union_ty)?;
1061    let finset_inter_ty = pi(
1062        BinderInfo::Implicit,
1063        "α",
1064        type0(),
1065        pi(
1066            BinderInfo::InstImplicit,
1067            "_inst",
1068            app(cst("DecidableEq"), bvar(0)),
1069            pi(
1070                BinderInfo::Default,
1071                "s",
1072                app(cst("Finset"), bvar(1)),
1073                pi(
1074                    BinderInfo::Default,
1075                    "t",
1076                    app(cst("Finset"), bvar(2)),
1077                    app(cst("Finset"), bvar(3)),
1078                ),
1079            ),
1080        ),
1081    );
1082    add_axiom(env, "Finset.inter", vec![], finset_inter_ty)?;
1083    let finset_to_set_ty = pi(
1084        BinderInfo::Implicit,
1085        "α",
1086        type0(),
1087        pi(
1088            BinderInfo::Default,
1089            "s",
1090            app(cst("Finset"), bvar(0)),
1091            app(cst("Set"), bvar(1)),
1092        ),
1093    );
1094    add_axiom(env, "Finset.toSet", vec![], finset_to_set_ty)?;
1095    let finset_sum_ty = pi(
1096        BinderInfo::Implicit,
1097        "α",
1098        type0(),
1099        pi(
1100            BinderInfo::Implicit,
1101            "β",
1102            type0(),
1103            pi(
1104                BinderInfo::InstImplicit,
1105                "_inst",
1106                app(cst("AddCommMonoid"), bvar(0)),
1107                pi(
1108                    BinderInfo::Default,
1109                    "s",
1110                    app(cst("Finset"), bvar(2)),
1111                    pi(BinderInfo::Default, "f", arrow(bvar(3), bvar(3)), bvar(3)),
1112                ),
1113            ),
1114        ),
1115    );
1116    add_axiom(env, "Finset.sum", vec![], finset_sum_ty)?;
1117    let card_empty_ty = pi(
1118        BinderInfo::Implicit,
1119        "α",
1120        type0(),
1121        mk_eq_expr(
1122            nat_ty(),
1123            app(cst("Finset.card"), cst("Finset.empty")),
1124            Expr::Lit(oxilean_kernel::Literal::Nat(0)),
1125        ),
1126    );
1127    add_axiom(env, "Finset.card_empty", vec![], card_empty_ty)?;
1128    let card_insert_ty = pi(
1129        BinderInfo::Implicit,
1130        "α",
1131        type0(),
1132        pi(
1133            BinderInfo::InstImplicit,
1134            "_inst",
1135            app(cst("DecidableEq"), bvar(0)),
1136            pi(
1137                BinderInfo::Implicit,
1138                "a",
1139                bvar(1),
1140                pi(
1141                    BinderInfo::Implicit,
1142                    "s",
1143                    app(cst("Finset"), bvar(2)),
1144                    pi(
1145                        BinderInfo::Default,
1146                        "h",
1147                        app(
1148                            cst("Not"),
1149                            app2(cst("Set.mem"), bvar(1), app(cst("Finset.toSet"), bvar(0))),
1150                        ),
1151                        mk_eq_expr(
1152                            nat_ty(),
1153                            app(
1154                                cst("Finset.card"),
1155                                app2(cst("Finset.insert"), bvar(2), bvar(1)),
1156                            ),
1157                            app(cst("Nat.succ"), app(cst("Finset.card"), bvar(1))),
1158                        ),
1159                    ),
1160                ),
1161            ),
1162        ),
1163    );
1164    add_axiom(env, "Finset.card_insert", vec![], card_insert_ty)?;
1165    let card_union_le_ty = pi(
1166        BinderInfo::Implicit,
1167        "α",
1168        type0(),
1169        pi(
1170            BinderInfo::InstImplicit,
1171            "_inst",
1172            app(cst("DecidableEq"), bvar(0)),
1173            pi(
1174                BinderInfo::Default,
1175                "s",
1176                app(cst("Finset"), bvar(1)),
1177                pi(
1178                    BinderInfo::Default,
1179                    "t",
1180                    app(cst("Finset"), bvar(2)),
1181                    app2(
1182                        cst("Nat.le"),
1183                        app(
1184                            cst("Finset.card"),
1185                            app2(cst("Finset.union"), bvar(1), bvar(0)),
1186                        ),
1187                        app2(
1188                            cst("Nat.add"),
1189                            app(cst("Finset.card"), bvar(1)),
1190                            app(cst("Finset.card"), bvar(0)),
1191                        ),
1192                    ),
1193                ),
1194            ),
1195        ),
1196    );
1197    add_axiom(env, "Finset.card_union_le", vec![], card_union_le_ty)?;
1198    Ok(())
1199}
1200/// Build `Set α` type expression.
1201#[allow(dead_code)]
1202pub fn mk_set(elem_ty: Expr) -> Expr {
1203    app(cst("Set"), elem_ty)
1204}
1205/// Build `Set.mem a s` expression.
1206#[allow(dead_code)]
1207pub fn mk_set_mem(elem: Expr, set: Expr) -> Expr {
1208    app2(cst("Set.mem"), elem, set)
1209}
1210/// Build `Set.union s t` expression.
1211#[allow(dead_code)]
1212pub fn mk_set_union(s: Expr, t: Expr) -> Expr {
1213    app2(cst("Set.union"), s, t)
1214}
1215/// Build `Set.inter s t` expression.
1216#[allow(dead_code)]
1217pub fn mk_set_inter(s: Expr, t: Expr) -> Expr {
1218    app2(cst("Set.inter"), s, t)
1219}
1220/// Build `Set.subset s t` expression.
1221#[allow(dead_code)]
1222pub fn mk_set_subset(s: Expr, t: Expr) -> Expr {
1223    app2(cst("Set.subset"), s, t)
1224}
1225/// Build `Set.diff s t` expression.
1226#[allow(dead_code)]
1227pub fn mk_set_diff(s: Expr, t: Expr) -> Expr {
1228    app2(cst("Set.diff"), s, t)
1229}
1230/// Build `Set.compl s` expression.
1231#[allow(dead_code)]
1232pub fn mk_set_compl(s: Expr) -> Expr {
1233    app(cst("Set.compl"), s)
1234}
1235/// Build `Set.image f s` expression.
1236#[allow(dead_code)]
1237pub fn mk_set_image(f: Expr, s: Expr) -> Expr {
1238    app2(cst("Set.image"), f, s)
1239}
1240/// Build `Set.preimage f s` expression.
1241#[allow(dead_code)]
1242pub fn mk_set_preimage(f: Expr, s: Expr) -> Expr {
1243    app2(cst("Set.preimage"), f, s)
1244}
1245/// Build `Set.range f` expression.
1246#[allow(dead_code)]
1247pub fn mk_set_range(f: Expr) -> Expr {
1248    app(cst("Set.range"), f)
1249}
1250/// Build `Set.singleton a` expression.
1251#[allow(dead_code)]
1252pub fn mk_set_singleton(a: Expr) -> Expr {
1253    app(cst("Set.singleton"), a)
1254}
1255/// Build `Set.insert a s` expression.
1256#[allow(dead_code)]
1257pub fn mk_set_insert(a: Expr, s: Expr) -> Expr {
1258    app2(cst("Set.insert"), a, s)
1259}
1260/// Build `Set.sep s p` expression.
1261#[allow(dead_code)]
1262pub fn mk_set_sep(s: Expr, p: Expr) -> Expr {
1263    app2(cst("Set.sep"), s, p)
1264}
1265/// Build `Set.empty` expression.
1266#[allow(dead_code)]
1267pub fn mk_set_empty() -> Expr {
1268    cst("Set.empty")
1269}
1270/// Build `Set.univ` expression.
1271#[allow(dead_code)]
1272pub fn mk_set_univ() -> Expr {
1273    cst("Set.univ")
1274}
1275/// Build `Finset α` type expression.
1276#[allow(dead_code)]
1277pub fn mk_finset(elem_ty: Expr) -> Expr {
1278    app(cst("Finset"), elem_ty)
1279}
1280/// Build `Finset.empty` expression.
1281#[allow(dead_code)]
1282pub fn mk_finset_empty() -> Expr {
1283    cst("Finset.empty")
1284}
1285/// Build `Finset.insert a s` expression.
1286#[allow(dead_code)]
1287pub fn mk_finset_insert(a: Expr, s: Expr) -> Expr {
1288    app2(cst("Finset.insert"), a, s)
1289}
1290/// Build `Finset.card s` expression.
1291#[allow(dead_code)]
1292pub fn mk_finset_card(s: Expr) -> Expr {
1293    app(cst("Finset.card"), s)
1294}
1295/// Build `Finset.union s t` expression.
1296#[allow(dead_code)]
1297pub fn mk_finset_union(s: Expr, t: Expr) -> Expr {
1298    app2(cst("Finset.union"), s, t)
1299}
1300/// Build `Finset.inter s t` expression.
1301#[allow(dead_code)]
1302pub fn mk_finset_inter(s: Expr, t: Expr) -> Expr {
1303    app2(cst("Finset.inter"), s, t)
1304}
1305/// Build `Finset.toSet s` expression.
1306#[allow(dead_code)]
1307pub fn mk_finset_to_set(s: Expr) -> Expr {
1308    app(cst("Finset.toSet"), s)
1309}
1310/// Build `Finset.sum s f` expression.
1311#[allow(dead_code)]
1312pub fn mk_finset_sum(s: Expr, f: Expr) -> Expr {
1313    app2(cst("Finset.sum"), s, f)
1314}