proposition: Lemma plift_on_top c1 x : on_top x (plift c1) = on_top x c1.
proof: Proof. apply/on_topP/on_topP => H d; have := H d; rewrite !ffunE => H1 H2; apply: H1. by rewrite H2. by apply: lift_inj H2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)