From e8c38a70678abe5b1f986b8a4d828e673ab6dec3 Mon Sep 17 00:00:00 2001 From: xsnow Date: Sat, 6 Apr 2024 08:18:51 +0800 Subject: [PATCH] Comment incomplete proofs --- proof/old_system/uni/algo_worklist/prop_basic.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proof/old_system/uni/algo_worklist/prop_basic.v b/proof/old_system/uni/algo_worklist/prop_basic.v index 5b81d8b6..16c32582 100644 --- a/proof/old_system/uni/algo_worklist/prop_basic.v +++ b/proof/old_system/uni/algo_worklist/prop_basic.v @@ -110,8 +110,8 @@ Proof. induction* HE. gen Σ1 A1 A2. induction Σ2; intros; cbn in *. - + inverts* HE. - - introv HB HT. clear a_wf_body_var_binds_another. + (* + inverts* HE. *) + (* - introv HB HT. clear a_wf_body_var_binds_another. *) Admitted. Lemma a_wf_exp_var_binds_another_cons : forall Σ1 x e A1 A2,