Skip to content

Commit

Permalink
minor improvement
Browse files Browse the repository at this point in the history
  • Loading branch information
HuStmpHrrr committed Dec 15, 2024
1 parent c049895 commit 7ba0096
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions theories/Core/Soundness/EqualityCases.v
Original file line number Diff line number Diff line change
Expand Up @@ -83,14 +83,14 @@ Proof.
eexists; repeat split; mauto.
- glu_univ_elem_econstructor; mauto 3; reflexivity.
- do 2 try econstructor; mauto 3;
try (intros Δ' τ **;
assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
applying_glu_rel_judge;
saturate_glu_typ_from_el;
bulky_rewrite).
intros Δ' τ **;
assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
applying_glu_rel_judge;
saturate_glu_typ_from_el;
bulky_rewrite.
Qed.

#[export]
Expand Down

0 comments on commit 7ba0096

Please sign in to comment.