proposition: Lemma refine_if_andb {A} : forall (i i' : bool) (t e : A), (if i then (if i' then t else e) else e) = if i && i' then t else e.
proof: Proof. destruct i; destruct i'; reflexivity. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics