From 6c4b4262ab1c379feecc84024b8c1521d55de5b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Fri, 2 Aug 2024 15:54:41 +0200 Subject: [PATCH] Minore repairs in Param --- theories/Param.v | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/theories/Param.v b/theories/Param.v index ddd0e14..a6af80b 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -5037,8 +5037,7 @@ Proof. eapply ctyping_subst. 2: eassumption. destruct (isKind mx) eqn:ek. - constructor. 1: rasimpl. 1: constructor. 1: rasimpl. - + rewrite <- !funcomp_assoc. - apply crtyping_typing. ertype. + + apply crtyping_typing. ertype. + cbn. split. * ertype. * eapply ccmeta_conv. 1: ertype. @@ -5049,8 +5048,7 @@ Proof. * eapply ccmeta_conv. 1: ertype. cbn. rasimpl. rewrite rinstInst'_cterm. reflexivity. - constructor. 1: rasimpl. 1: constructor. 1: rasimpl. - + rewrite <- !funcomp_assoc. - apply crtyping_typing. ertype. + + apply crtyping_typing. ertype. + cbn. split. * ertype. * eapply ccmeta_conv. 1: ertype. @@ -5077,8 +5075,7 @@ Proof. - ertype. eapply ccmeta_conv. + eapply ctyping_subst. 2: ertype. cbn. constructor. 1: rasimpl. 1: constructor. 1: rasimpl. - * rewrite <- !funcomp_assoc. - apply crtyping_typing. ertype. + * apply crtyping_typing. ertype. * { cbn. split. - ertype. @@ -5216,8 +5213,7 @@ Proof. - eapply ctyping_subst. 2: ertype. destruct (isKind mx) eqn:ekx. + constructor. 1: rasimpl. 1: constructor. 1: rasimpl. - * rewrite <- !funcomp_assoc. - apply crtyping_typing. ertype. + * apply crtyping_typing. ertype. * { cbn. split. - ertype. @@ -5232,8 +5228,7 @@ Proof. cbn. rasimpl. rewrite rinstInst'_cterm. reflexivity. } + constructor. 1: rasimpl. 1: constructor. 1: rasimpl. - * rewrite <- !funcomp_assoc. - apply crtyping_typing. ertype. + * apply crtyping_typing. ertype. * { cbn. split. - ertype.