proposition: Lemma hemiMetric_wd :forall (e1 e2:Q), (e1 == e2) -> forall A1 A2, (forall x, A1 x <-> A2 x) -> forall B1 B2, (forall x, B1 x <-> B2 x) -> (hemiMetric e1 A1 B1 <-> hemiMetric e2 A2 B2).
proof: Proof. cut (forall e1 e2 : Q, e1 == e2 -> forall A1 A2 : X -> Prop, (forall x : X, A1 x <-> A2 x) -> forall B1 B2 : X -> Prop, (forall x : X, B1 x <-> B2 x) -> (hemiMetric e1 A1 B1 -> hemiMetric e2 A2 B2)). intros; split. eauto. symmetry in H0. assert (H1':forall x : X, A2 x <-> A1 x) by firstorder. assert (H2':forall x : X, B2 x <-> B1 x) by firstorder. eauto. intros e1 e2 He A1 A2 HA B1 B2 HB H x Hx. rewrite <- HA in Hx. destruct (H x Hx) as [HG | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. change (e1 == e2) in He. rewrite <- HB. split. exact Hy0. rewrite <- He. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.logic.Classic CoRN.metric2.Metric CoRN.metric2.Classification Coq.Lists.List Coq.ZArith.ZArith CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax