+(*
+lemma insert_sorted:
+ \forall A:Set. \forall le:A\to A\to bool.
+ (\forall a,b:A. le a b = false \to le b a = true) \to
+ \forall l:list A. \forall x:A.
+ ordered A le l = true \to ordered A le (insert A le x l) = true.
+ intros (A le H l x K).
+ letin P ≝ (\lambda ll. ordered A le ll = true).
+ fold simplify (P (insert A le x l)).
+ apply (
+ let rec insert_ind (l: list A) \def
+ match l in list return λli. l = li → P (insert A le x li) with
+ [ nil ⇒ (? : l = [] → P [x])
+ | (cons he l') ⇒
+ match le x he
+ return
+ λb. le x he = b → l = he::l' → P (match b with
+ [ true ⇒ x::he::l'
+ | false ⇒ he::(insert A le x l') ])
+ with
+ [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
+ | false ⇒
+ (? : \forall lrec. P (insert A le x lrec) \to
+ le x he = false → l = he::l' → P (he::(insert A le x l')))
+ l' (insert_ind l')
+ ]
+ (refl_eq ? (le x he))
+ ] (refl_eq ? l) in insert_ind l);
+
+ intros; simplify;
+ [ rewrite > H1;
+ apply andb_elim; simplify;
+ generalize in match K; clear K;
+ rewrite > H2; intro;
+ apply H3
+ |
+ | reflexivity
+ ].
+
+
+
+
+
+
+ [ rewrite > H1; simplify;
+ generalize in match (ordered_injective A le l K);
+ rewrite > H2; simplify; intro; change with (ordered A le l' = true).
+ elim l'; simplify;
+ [ reflexivity
+ |
+
+
+ rewrite > H1; simplify.
+ elim l'; [ reflexivity | simplify;
+ | simplify.
+ | reflexivity.
+ ].
+*)
+