proposition: Lemma nth_eq: forall (a b: list bool), (length a) = (length b) -> (forall (i: nat), (i < length a)%nat -> nth i a false = nth i b false) -> a = b.
proof: Proof. intros a. induction a as [ | a xs IHxs]. - intros. simpl in *. symmetry in H. now rewrite empty_list_length in H. - intros [ | b ys] H0. + simpl in *. now contradict H0. + specialize (@IHxs ys). inversion H0. specialize (@IHxs H1). intros. pose proof (@H 0%nat). simpl in H2. cut ((0 < S (Datatypes.length xs))%nat). intro HS. specialize (@H2 HS). rewrite H2; apply f_equal. apply IHxs. intros. apply (@nth_eq0 i a b xs ys). apply H. simpl. lia. lia. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance