proposition: Theorem RF_Encrypt_length_incr : forall a b c d, In (a, b) (getSupport (RF_Encrypt c d)) -> (length b <= 1 + length c)%nat.
proof: Proof. intuition. unfold RF_Encrypt in *. repeat simp_in_support. destruct x0. repeat simp_in_support. unfold PRFE_RandomFunc, randomFunc in *. destruct (arrayLookup (Bvector_EqDec eta) c x); repeat simp_in_support; simpl in *; lia. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime