Helper

project_extend_id

Section fiber_nd

Type Lemma

Proof Lines 4

Lemma project_extend_id (u : 'I_n.+1 -> msg) (target : msg) (w : {ffun 'I_n -> msg}) : project_fiber (extend_to_fiber u target w) = w.

project then extend is identity

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...