Classify theorem as theorem

Beluga-lang · Jun 12, 2024 · a71f0ca · a71f0ca
1 parent 9cb1b81
commit a71f0ca
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Core/Completeness.v b/theories/Core/Completeness.v
@@ -20,7 +20,7 @@ Proof with mautosolve.
   unshelve epose proof (per_elem_then_per_top _ _ (length Γ)) as [? []]; shelve_unifiable...
 Qed.
 
-Lemma completeness_for_typ_subsumption : forall {Γ A A'},
+Theorem completeness_for_typ_subsumption : forall {Γ A A'},
   {{ Γ ⊢ A ⊆ A' }} ->
   exists i W W', nbe Γ A {{{ Type@i }}} W /\ nbe Γ A' {{{ Type@i }}} W' /\ nf_subsumption W W'.
 Proof.