[STATEMENT]
lemma rg_fo_inv[simp]: "residualGraph c (flow_of_cf cf) = cf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
using rg_is_cf
[PROOF STATE]
proof (prove)
using this:
f.cf = cf

goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
cf_of (flow_of_cf cf) = cf

goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
.