proposition: Lemma create_extensionality : forall o m c i s o1 m1 c1 i1 s1, o = o1 -> m = m1 -> (forall u v, inc u m -> inc v m -> source u = target v -> c u v = c1 u v) -> (forall x, inc x o -> i x = i1 x) -> s = s1 -> create o m c i s = create o1 m1 c1 i1 s1.
proof: Proof. ir. wr H. wr H0. assert (lem1: L m (fun u => L (Z m (fun v => source u = target v)) (c u)) = L m (fun u => L (Z m (fun v => source u = target v)) (c1 u))). ap Function.create_extensionality. tv. ir. ap Function.create_extensionality. tv. ir. ap H1. am. Ztac. Ztac. assert (lem2: L o i = L o i1). ap Function.create_extensionality. tv. au. uf create. rw lem1. rw lem2. rw H3. reflexivity. Qed.
imports: Arith universe