proposition: Lemma split_rdp_step_top : forall R f g ls lt, rdp_step (axiom (ddp (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1))))) R (Term g lt) (Term f ls) -> ( (defined (@union _ R1 R2) f /\ defined (@union _ R1 R2) g) \/ (defined R3 f /\ defined R3 g) \/ (defined R3 f /\ defined (@union _ R1 R2) g)).
proof: Proof. intros R f g ls lt H; inversion H as [f' l1 l2 t3 H' H'']; subst. apply (split_dp_top f g l2 lt); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)