proposition: Lemma StronglySorted_rec : forall P:list A -> Type, P [] -> (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> forall l, StronglySorted l -> P l.
proof: Proof. firstorder using StronglySorted_rect. Qed.
imports: List Relations Relations_1