proposition: Lemma StronglySorted_rect : 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. intros P ? ? l; induction l; firstorder using StronglySorted_inv. Defined.
imports: List Relations Relations_1