proposition: Lemma NUMSUM_INJ : forall b1 : Prop, forall x1 : nat, forall b2 : Prop, forall x2 : nat, ((NUMSUM b1 x1) = (NUMSUM b2 x2)) = ((b1 = b2) /\ (x1 = x2)).
proof: Proof. intros b1 x1 b2 x2. apply prop_ext. 2: intros [e1 e2]; subst; reflexivity. unfold NUMSUM. unfold NUMERAL, BIT1, BIT0. destruct (prop_degen b1); destruct (prop_degen b2); subst; try rewrite !COND_True; try rewrite !COND_False; intro e. split. auto. lia. apply False_rec. lia. apply False_rec. lia. split. auto. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance