proposition: Lemma list_eq_bool_ok : forall A eq_bool (eq_bool_ok : forall a1 a2, match eq_bool a1 a2 with true => a1 = a2 | false => a1 <> a2 end) (l1 l2 : list A), match list_eq_bool eq_bool l1 l2 with true => l1 = l2 | false => l1 <> l2 end.
proof: Proof. intros A eq_bool eq_bool_ok. fix list_eq_bool_ok 1; intro l1; case l1; clear l1; [idtac | intros a1 l1]; (intro l2; case l2; clear l2; [idtac | intros a2 l2]). simpl; reflexivity. simpl; discriminate. simpl; discriminate. simpl; generalize (eq_bool_ok a1 a2); case (eq_bool a1 a2); [intro a1_eq_a2 | intro a1_diff_a2]; simpl. generalize (list_eq_bool_ok l1 l2); case (list_eq_bool eq_bool l1 l2); [intro l1_eq_l2 | intro l1_diff_l2]. apply f_equal2; assumption. intro a1l1_eq_a2l2; apply l1_diff_l2; injection a1l1_eq_a2l2; intros; assumption. intro a1l1_eq_a2l2; apply a1_diff_a2; injection a1l1_eq_a2l2; intros; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)