proposition: Lemma collapse_ifs_dec : forall P (b: {P} + {~P}), (if (if b then true else false) then true else false) = (if b then true else false).
proof: Proof. destruct b; reflexivity. Qed.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Bool.Bool Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat