ordered A le l = true \to ordered A le (insert A le x l) = true.
intros 5 (A le H l x).
apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
ordered A le l = true \to ordered A le (insert A le x l) = true.
intros 5 (A le H l x).
apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));