proposition: Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) , eval_bf env (map_bformula fct f) = eval_bf (fun b x => env b (fct x)) f.
proof: Proof. intros T U fct env k f; induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf |? ? IHf1 ? ? IHf2|? ? IHf1 ? IHf2|? IHf1 ? IHf2]; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. rewrite <- IHf. auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid