proposition: Theorem hlist_nth_hlist_app : forall l l' (h : hlist l) (h' : hlist l') n, hlist_nth (hlist_app h h') n = match nth_error l n as k return nth_error l n = k -> match nth_error (l ++ l') n return Type with | None => unit | Some t => F t end with | Some _ => fun pf => match cast1 _ _ _ pf in _ = z , eq_sym pf in _ = w return match w return Type with | None => unit | Some t => F t end -> match z return Type with | None => unit | Some t => F t end with | eq_refl , eq_refl => fun x => x end (hlist_nth h n) | None => fun pf => match cast2 _ _ _ pf in _ = z return match z with | Some t => F t | None => unit end with | eq_refl => hlist_nth h' (n - length l) end end eq_refl.
proof: Proof. induction h; simpl; intros. { destruct n; simpl in *; reflexivity. } { destruct n; simpl. { reflexivity. } { rewrite IHh. reflexivity. } } Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms