proposition: Lemma one_step_ind2 : forall (R : relation term) (P : forall t t0 : term, one_step R t t0 -> Prop) (P0 : forall l l0 : list term, one_step_list (one_step R) l l0 -> Prop), (forall (t1 t2 : term) (a : axiom R t1 t2), P t1 t2 (at_top R t1 t2 a)) -> (forall (f0 : symbol) (l1 l2 : list term) (o : one_step_list (one_step R) l1 l2), P0 l1 l2 o -> P (Term f0 l1) (Term f0 l2) (in_context R f0 l1 l2 o)) -> (forall (t1 t2 : term) (l : list term) (o : one_step R t1 t2), P t1 t2 o -> P0 (t1 :: l) (t2 :: l) (head_step (one_step R) t1 t2 l o)) -> (forall (t : term) (l1 l2 : list term) (o : one_step_list (one_step R) l1 l2), P0 l1 l2 o -> P0 (t :: l1) (t :: l2) (tail_step t o)) -> forall (t t0 : term) (o : Eqt.one_step R t t0), P t t0 o .
proof: Proof. intros R P P0 H H0 H1 H2. fix one_step_ind2 3. intros t t0 [t1 t2 a|f l1 l2 o]. apply H. apply H0. revert l1 l2 o. fix one_step_list_ind2 3 . intros l1 l2 [t1 t2 l a|t1 l1' l2' a]. apply H1. apply one_step_ind2. apply H2. apply one_step_list_ind2. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)