We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e5cd005 commit 22a72a6Copy full SHA for 22a72a6
nominal/lambda.mm1
@@ -148,7 +148,7 @@ theorem freshness_irrelevance (exp_pred exp_suff_fresh: Pattern)
148
rsyl (anl eVar_in_subset) @
149
lc_lemma_3 exp_pred_sorting exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs));
150
151
-theorem prototype_induction_principle (exp_pred exp_suff_fresh: Pattern)
+theorem induction_principle (exp_pred exp_suff_fresh: Pattern)
152
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
153
(exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
154
(exp_pred_sorting: $ is_of_sort exp_pred Exp $)
0 commit comments