From 1fd96bbff0b21606fbd1a7809c8340abc2d54e78 Mon Sep 17 00:00:00 2001 From: HuStmpHrrr Date: Sat, 23 Nov 2024 11:35:54 -0800 Subject: [PATCH] leftover --- theories/Core/Completeness/EqualityCases.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Core/Completeness/EqualityCases.v b/theories/Core/Completeness/EqualityCases.v index 74243e7..559321a 100644 --- a/theories/Core/Completeness/EqualityCases.v +++ b/theories/Core/Completeness/EqualityCases.v @@ -1,9 +1,9 @@ From Coq Require Import Morphisms_Relations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import ContextCases LogicalRelation SubstitutionCases SubtypingCases TermStructureCases UniverseCases VariableCases. -From Mcltt.Core.Semantic Require Import Realizability. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import ContextCases LogicalRelation SubstitutionCases SubtypingCases TermStructureCases UniverseCases VariableCases. +From Mctt.Core.Semantic Require Import Realizability. Import Domain_Notations. Lemma rel_exp_eq_cong : forall {Γ i A A' M1 M1' M2 M2'},