Some trivial coq tactics whose purpose is to automagically extract/fold particular subterms of the goal type. The idea is to reduce ambiguity in human/coq interactions.

subterms.v

Require Import HoTT. 

(* or your favourite source for the needed arrithmetic types *)

Open Scope list_scope.

(** 
  These are tactics to aid human consumption/production of terms compatible
  with the goal type --- sometimes coq prettyprinting produces ambiguous 
  appearances, while refine fails unless you fill in more holes --- which is
  hard to do if the first refinement coq finds for an ambiguously-filled hole
  is wrong! Happily, we don't need coq to have sneakier pattern matching/
  unification : coq already knows all the subterms of the goal, and can pull
  them out for us! here are some trivial ways of doing this. Someone cleverer
  than I with Ltac or such can figure out how to customize the names of terms
  at runtime, how to make parameters optional, etc.
  
  I emphasize: these are intended to aid human interaction; I see little use
  to calling them from your own Ltac scripts.  For instance, folding terms
  into definitional hypotheses makes it harder for later tactics to get hold
  of them! Ltac doesn't seem to have tools for reference by name. And that's OK.
  *)

Ltac inLHS :=
  match goal with
  | |- ?A = ?B =>
    let H := fresh "lhs" in 
    set (H := A)
  | _ => idtac "nothing to do" end.

Ltac inRHS :=
  match goal with
  | |- ?A = ?B =>
    let H := fresh "rhs" in 
    set (H := B)
  | _ => idtac "nothing to do" end.

(** Danger, Gill Robertsvale!  it's more than possible these coercions
  may break lots of things! That is, it's more than credible that making
  more expressions meaningful will hide where errors are happening
  later on.
*)

Definition lib := list Bool.
Definition apb : lib -> lib -> lib := (@app Bool).
Coercion apb : lib >-> Funclass.
Definition quotb : Bool -> lib :=
  fun b => (cons b nil).
Coercion quotb : Bool >-> lib.

Notation bt := true.
Notation bf := false.

(** so now, we can 
 :< Check ( bt bt bt bf bf bt bf bt bt bt ) 
 is a (list Bool), or (lib).  It might also be a (lib -> lib), if necessary, but
 not now, it isn't!
 *)

(** we assume a binary tree model for all terms, which is in fact correctish!
  however, while the natural address for a subtree of a binary tree is a binary
  string, it's much easier to write numbers than binary strings ; and you can
  all do base-2 arrithmetic in base-10, right?
 *)

Ltac subTermOf anum Thing := 
  let  z := eval vm_compute (* so we can just write our ( bft ) string and it'll work *)
   in anum in 
  match Thing with
  | ?A ?B => match z with 
   | nil => Thing
   | true => A (* because we don't want to be writing ( bf : lib ) all the time ... *)
   | false => B (* ... coercions are lazy, which is the Right Thing *)
   | cons true ?num => subTermOf num A
   | cons false ?num => subTermOf num B
      end
  | _ => Thing
  end.

Ltac goalSubTerm anum :=
  let H := fresh "subterm" in
  match goal with
  | |- ?T =>
    let w := subTermOf anum T in
    pose ( H := w ) end.
    
Ltac goalSubTermN anum nom :=
  let H := fresh nom in
  match goal with
  | |- ?T =>
    let w := subTermOf anum T in
    pose ( H := w ) end.

(** this version, using set instead of pose, folds the newly named subterm
  wherever coq thinks it appears. This may not mean that every *convertible*
  subterm gets folded, just those that don't take work.
  Since this changes the parse tree, [foldSubTerm]s are not commutative!
  ( More detail: strictly, the tree is only pruned a little, 
    so
     [foldSubTerm 10w ; foldSubTerm 1w]
    is quite reasonable, but
     [foldSubTerm 1w ; foldSubTerm 10w ]
    gives a [subtermN := _ : _ |- _ ] and a [ subtermN' := subtermN : _ |- _ ]
    which probably isn't what you wanted. )
   *)

Ltac foldSubTerm anum :=
  let H := fresh "subterm" in
  match goal with
  | |- ?T =>
    let w := subTermOf anum T in
    set ( H := w ) in * end.
    
Ltac foldSubTermN anum nom :=
  let H := fresh nom in
  match goal with
  | |- ?T =>
    let w := subTermOf anum T in
    set ( H := w ) in * end.

Ltac introSubTerm n thing :=
  let w := subTermOf n thing in
   let H := fresh "subterm" in
    pose ( H := w ).

Ltac dependOnLastH :=
  match goal with
  | [ f := _ : _ |- _ ] =>
      try clearbody f;
      revert f
  | [ f : _ |- _ ] => revert f 
  | _ => idtac "it had better be true!" end;
   match goal with
   | |- forall x, @?T x => let g := fresh "f" in
     pose (g := T) ; intros
   | _ => idtac "i'm confused" end.

Ltac dependOnLastTwo :=
  try match goal with
    | [ f : _ , gf : _ |- _ ] =>
      try clearbody gf; try clearbody f;
      revert f gf
    | _ => idtac "maybe there's only one?"
    end;
    
    match goal with
      | |- forall x, forall y, @?T x y =>
        let h := fresh "fTwo" in
          pose ( h := T ) ; intros
      | _ => idtac "i'm confused."
       end.

Ltac remember_as thing name :=
  let H := fresh name 
    with Heq := fresh name "_eq" in
   set ( H := thing ) in * ;
   assert ( Heq := idpath : H = thing );
   clearbody H.

In the latest revision, exploit coq's magic Coercion engine to enable really tidy notations for lists of Booleans. Of course, you could do the same for nearly any type in the place of Bool, but I don't think I recommend it. This will break scripts actually using subTermOf, but translating them isn't hard.