attrs:Cic.attribute list ->
(proof_status -> 'a) -> (* init data *)
(proof_status * 'a -> proof_status -> 'a) -> (* update data *)
attrs:Cic.attribute list ->
(proof_status -> 'a) -> (* init data *)
(proof_status * 'a -> proof_status -> 'a) -> (* update data *)