proposition: Lemma cput_then_fail T1 T2 T1' e (s1' : coq_type T1') (r2 : loc T2) (s2 : coq_type T2) (r1 : loc T1) (s1 : coq_type T1) : nth_error (ofEnv e) (loc_id r1) = Some (mkbind s1') -> ~~ coercible T1 s1' -> (cput r2 s2 >> cput r1 s1) e = fail.
proof: Proof. move=> Hr1 T1s'. have [v Hr2|T2' v Hr2 T2v|Hr2] := ntherrorP e r2; last first. - by rewrite MS_bindE None_cput. - by rewrite MS_bindE (nocoerce_cput _ _ T2v). - rewrite MS_bindE (Some_cputE _ Hr2). rewrite bindE/=. have [Hr|Hr] := eqVneq (loc_id r1) (loc_id r2). + rewrite {1}/cput -Hr /= nth_error_set_nth. have [HT|HT] := eqVneq T1 T2; last by rewrite coerce_None. subst T2. rewrite coerce_Some//=. move: Hr1; rewrite Hr Hr2 => -[?]; subst T1' => _. by rewrite coercible_Some // in T1s'. + rewrite (nocoerce_cput _ _ T1s')//=. by rewrite (@nth_error_set_nth_other _ _ _ _ _ (mkbind s1')). Qed.
imports: JMeq mathcomp(all_ssreflect finmap) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer monad_model