typo

Beluga-lang · Dec 16, 2024 · d622157 · d622157
1 parent c01fbc9
commit d622157
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -650,7 +650,7 @@ Proof.
     handle_functional_glu_univ_elem.
     trivial.
 Qed.
-xb
+
 Lemma glu_univ_elem_per_subtyp_trm_conv : forall {i j k a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} ->