Prove cumulativity

Beluga-lang · May 8, 2024 · 93e1ec9 · 93e1ec9
1 parent 3bfedb1
commit 93e1ec9
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
@@ -346,3 +346,19 @@ Proof with solve [mauto].
       firstorder (econstructor; eauto).
   - split; try per_univ_elem_econstructor...
 Qed.
+
+Lemma per_univ_elem_cumu : forall {i a0 a1 R},
+    {{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
+    {{ DF a0 ≈ a1 ∈ per_univ_elem (S i) ↘ R }}.
+Proof.
+  simpl.
+  induction 1 using per_univ_elem_ind; subst.
+  - eapply per_univ_elem_core_univ'.
+    lia.
+  - per_univ_elem_econstructor.
+  - per_univ_elem_econstructor; mauto.
+    intros.
+    destruct_rel_mod_eval.
+    econstructor; mauto.
+  - per_univ_elem_econstructor; mauto.
+Qed.