proposition: Lemma rdp_step_equiv_strong : forall R1 R2 R3 R4 (R1_dp_equiv_R2: forall l r, dp R1 r l <-> dp R2 r l) (R3_equiv_R4 : forall l r, R3 r l <-> R4 r l) r l, rdp_step (axiom (ddp R1)) R3 r l <-> rdp_step (axiom (ddp R2)) R4 r l.
proof: Proof. intros R0 R4 R5 R6 R1_dp_equiv_R2 R3_equiv_R4 r l. split;intros H;case H;clear H; clear l r. intros f l1 l2 v H1 H2. inversion H2 as [t1 t2 sigma H2']; inversion H2' as [H2'' Sub]. constructor 1 with l2. rewrite <- (@rwr_list_equiv _ _ R3_equiv_R4); assumption. rewrite <- H0; constructor 1; split. rewrite <- R1_dp_equiv_R2; assumption. assumption. intros f l1 l2 v H1 H2. inversion H2 as [t1 t2 sigma H2']; inversion H2' as [H2'' Sub]. constructor 1 with l2. rewrite (@rwr_list_equiv _ _ R3_equiv_R4); assumption. rewrite <- H0; constructor 1; split. rewrite R1_dp_equiv_R2; assumption. assumption. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)