fact: Definition unpair {A B : type} (e : expr (Prod A B)) : option (expr A * expr B) := match e in expr T return unpair_type T with | Pair e1 e2 => Some (e1, e2) | _ => None end.
imports: Hammer(Tactics) Program.Equality Arith String