proposition: Lemma StepF_ind2 : forall (X Y : RSetoid) (P : StepF X -> StepF Y -> Prop), (forall (s s0 : StepF X) (t t0 : StepF Y), (s==s0) -> (t==t0) -> P s t -> P s0 t0) -> (forall (x:X) (y:Y), P (constStepF x) (constStepF y)) -> (forall (o : OpenUnit) (s s0 : StepF X) (t t0 : StepF Y), P s t -> P s0 t0 -> P (glue o s s0) (glue o t t0)) -> forall (s:StepF X) (t:StepF Y), P s t.
proof: Proof. intros X Y P wd c0 c1. induction s. induction t. apply c0. apply wd with (s:=(glue o (constStepF x) (constStepF x))) (t:=glue o t1 t2); try reflexivity. apply (glueSplit (constStepF x) o). apply c1; assumption. intros t. eapply wd. reflexivity. apply glueSplit with (a:=o). apply c1; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields