proposition: Lemma lattice_for_rect_pull {A B C} f t c b v : f (@lattice_for_rect A (fun _ => B) t c b v) = @lattice_for_rect A (fun _ => C) (f t) (fun x => f (c x)) (f b) v.
proof: Proof. destruct v; reflexivity. Qed.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Tactics.SplitInContext Fiat.Common.Notations