From 01f92c302715aacaac01d57f62710b55968a8713 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 18 Jun 2025 10:41:08 +0200 Subject: [PATCH] rm eta-expansion in lift_wf_term_it_impl --- common/theories/EnvironmentTyping.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v index 385f66397..ae384445f 100644 --- a/common/theories/EnvironmentTyping.v +++ b/common/theories/EnvironmentTyping.v @@ -367,15 +367,15 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). Definition lift_typing_conj (P Q : context -> _) := lift_typing1 (Prop_local_conj P Q). - Lemma lift_wf_term_it_impl {P Q} {tm tm' : option term} {t t' : term} {u u' r r'} : - forall tu: lift_wf_term P (Judge tm t u r), - match tm', tm with None, _ => unit | Some tm', Some tm => P tm -> Q tm' | _, _ => False end -> - (P t -> Q t') -> - lift_wf_term Q (Judge tm' t' u' r'). + Lemma lift_wf_term_it_impl {P Q} {j j'} : + forall tu: lift_wf_term P j, + match j_term j', j_term j with None, _ => unit | Some tm', Some tm => P tm -> Q tm' | _, _ => False end -> + (P (j_typ j) -> Q (j_typ j')) -> + lift_wf_term Q j'. Proof. intros (Htm & Hs) HPQc HPQs. split; auto. - destruct tm, tm' => //=. now apply HPQc. + destruct (j_term j), (j_term j') => //=. now apply HPQc. Qed. Lemma lift_wf_term_f_impl P Q tm t u u' r r' :