proposition: Lemma interp_bformula_le_gen : forall k f, P k f.
proof: Proof. intro k. induction f as [k|k|k t|k t a|k f1 IHf1 f2 IHf2|k f1 IHf1 f2 IHf2|k f1 IHf1|k f1 IHf1 o f2 IHf2|k f1 IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; unfold P in *; try (destruct k; simpl; tauto); try (destruct k; simpl; unfold is_true;rewrite andb_true_iff;intros (H1,H2);rewrite IHf1, IHf2;tauto). - destruct k; simpl; destruct t;unfold bounded_formula;simpl; unfold is_true;rewrite andb_true_iff;intros (H1, H2); rewrite !(interp_pexpr_le _ _ Hnth);tauto. - destruct k; simpl; intro H; now rewrite IHf1. - destruct k; simpl. + unfold is_true;rewrite andb_true_iff;intros (H1, H2). split. * intros H3 H4. rewrite <- IHf2; auto. apply H3. now rewrite IHf1. * intros H3 H4. rewrite IHf2; auto. apply H3. now rewrite <- IHf1. + unfold is_true;rewrite andb_true_iff;intros (H1, H2). now rewrite IHf1, IHf2. - simpl. unfold is_true;rewrite andb_true_iff;intros (H1, H2). now rewrite IHf1, IHf2. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz