proposition: Lemma list_lt_trans : forall (x y z : list A), list_lt x y -> list_lt y z -> list_lt x z.
proof: Proof. induction x as [ |x xs IHxs]; intros [ |y ys] [ |z zs]; simpl; auto. - inversion 1. - intros [H1|[H1a H1b]] [H2|[H2a H2b]]. + left; eapply lt_trans; eauto. + left. unfold is_true in H2a. rewrite eqb_spec in H2a. now subst z. + left. unfold is_true in H1a. rewrite eqb_spec in H1a. now subst y. + right. split. * unfold is_true in H1a. rewrite eqb_spec in H1a. now subst y. * eapply IHxs; eauto. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes